fact: Definition parse (str : string) : optionE com := let tokens := tokenize str in match parseSequencedCommand bignumber tokens with | SomeE (c, []) => SomeE c | SomeE (_, t::_) => NoneE ("Trailing tokens remaining: " ++ t) | NoneE err => NoneE err end.
imports: Coq(Strings.String) Coq(Strings.Ascii) Coq(Arith.Arith) Coq(Init.Nat) Coq(Arith.EqNat) Coq(Lists.List) LF(Maps Imp)