fact: Record pregrammar' (Char : Type) := { pregrammar_productions :> list (string * productions Char); pregrammar_nonterminals : list string := map fst pregrammar_productions; invalid_nonterminal : string := gensym pregrammar_nonterminals; Lookup_idx : nat -> productions Char := fun n => nth n (map snd pregrammar_productions) nil; Lookup_string : string -> productions Char := list_to_productions nil pregrammar_productions; nonterminals_unique : NoDupR string_beq pregrammar_nonterminals }.
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