fact: Record pregrammar Char := { pregrammar_rproductions : list (string * rproductions Char); pregrammar_idata : interp_RCharExpr_data Char; pregrammar_rnonterminals : list string := map fst pregrammar_rproductions; rnonterminals_unique : NoDupR string_beq pregrammar_rnonterminals; RLookup_idx : nat -> rproductions Char := fun n => nth n (map snd pregrammar_rproductions) nil }.
imports: Coq.Strings.String Coq.Lists.List Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.Gensym