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.Arith.EqNat Coq.Lists.List Maps Imp