fact: Record Parser (Toks : nat -> Type) (Tok : Type) (M : Type -> Type) (A : Type) (n : nat) : Type := MkParser { runParser {m} : m <= n -> Toks m -> M (Success Toks Tok A m) }.
imports: Coq(PeanoNat) parseque(Category Induction Sized NEList Success EqDec)