fact: Record grammar := { Start_symbol :> string; Lookup :> string -> productions; Start_productions :> productions := Lookup Start_symbol; Valid_nonterminals : list string; Valid_productions : list productions := map Lookup Valid_nonterminals }.
imports: Coq.Strings.String Coq.Lists.List Fiat.Parsers.StringLike.Core