fact: Fixpoint state_of_parse str pats (p : parse_of G str pats) := @state_of_parse' (@state_of_parse) (@state_of_parse_production) str pats p with state_of_parse_production str pat (p : parse_of_production G str pat) := @state_of_parse_production' (@state_of_parse_production) (@state_of_parse_item) str pat p with state_of_parse_item str it (p : parse_of_item G str it) := @state_of_parse_item' (@state_of_parse) str it p.
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