fact: Definition parseAscii_as_nat (v : ascii) : nat := Nat.modulo (1 + nat_of_ascii v - nat_of_ascii "1"%char) 10.
imports: Coq.Strings.String Coq.Lists.List Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Common.Notations