fact: Fixpoint many_helper {T} (p : parser T) acc steps xs := match steps, p xs with | 0, _ => NoneE "Too many recursive calls" | _, NoneE _ => SomeE ((rev acc), xs) | S steps', SomeE (t, xs') => many_helper p (t :: acc) steps' xs' end.
imports: Coq(Strings.String) Coq(Strings.Ascii) Coq(Arith.Arith) Coq(Init.Nat) Coq(Arith.EqNat) Coq(Lists.List) LF(Maps Imp)