fact: Definition state_of_parse_production' str pat (p : parse_of_production G str pat) : ensemble_result str (fold_production' (lookup_state fold_grammar) (opt.compile_production pat)) := match p with | ParseProductionNil Hlen => {| er_state := on_nil_production; er_ensemble := ensemble_on_nil_production; er_related := on_nil_production_correct (prerelated := prerelated); er_correct := Hlen; er_state_le := reflexivity (R := state_le) _ |} | ParseProductionCons n pat pats p' p's => er_combine_production n str (state_of_parse_item p') (state_of_parse_production p's) end.
imports: Coq.Sets.Ensembles Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Fix.FromAbstractInterpretationDefinitions Fiat.Parsers.ContextFreeGrammar.Fix.Fix Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Common