fact: Record pregrammar_with_actions := { pregrammar_arproductions : list (string * rproductions_with_actions); pregrammar_aidata : interp_RCharExpr_data Char; pregrammar_arnonterminals : list string := map fst pregrammar_arproductions; pregrammar_a_only_rproductions : list (rproductions Char) := map (map (@projT1 _ _)) (map snd pregrammar_arproductions); arnonterminals_unique : NoDupR string_beq pregrammar_arnonterminals }.
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