fact: Record ParserReflective (G : pregrammar Ascii.ascii) := { rhas_parse : polyhas_parse_term cbool; rhas_parse_correct : rhas_parse = polypnormalize (parse_nonterminal_reified G (Start_symbol G)) }.
imports: Fiat.Parsers.BooleanRecognizerOptimizedReflective Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.ParserSyntax Fiat.Parsers.Reflective.ParserPartialUnfold