fact: Definition parseIdentifier (xs : list token) : optionE (string * list token) := match xs with | [] => NoneE "Expected identifier" | x::xs' => if forallb isLowerAlpha (list_of_string x) then SomeE (x, xs') else NoneE ("Illegal identifier:'" ++ x ++ "'") end.
imports: Coq(Strings.String) Coq(Strings.Ascii) Coq(Arith.Arith) Coq(Init.Nat) Coq(Arith.EqNat) Coq(Lists.List) LF(Maps Imp)