fact: Definition text (t : String) `{NonEmpty ascii t} : Parser Chars ascii M String n := Combinators.map NEList.toList (exacts nonEmpty).
imports: parseque(Category Induction Combinators Sized NEList Numbers) Coq(Ascii String) parseque(StringAsList) Coq(List)