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