proposition: Lemma parse_nonterminal_opt_eq {HSLP : StringLikeProperties Char} {splitdata_correct : @boolean_parser_completeness_dataT' _ _ _ G data} (str : String) (nt : String.string) : @GenericCorrectnessBaseTypes.parse_nt_is_correct _ _ _ _ _ simple_gencdata2 str (of_nonterminal nt) (GenericRecognizerMin.parse_nonterminal str nt) (proj1_sig (parse_nonterminal_opt str nt)).
proof: Proof. let p := match goal with |- context[proj1_sig ?p] => p end in rewrite (proj2_sig p). refine (proj2 (@parse_nonterminal_optdata_eq _ _ _ G splitdata simple_gendata simple_gencdata2 _ _ str nt _ ) _). unfold parse_nonterminal. exact (GenericRecognizerMin.parse_nonterminal_correct (gcdata := simple_gencdata2) str nt). Qed.
imports: Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.BaseTypes Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.SimpleRecognizer Fiat.Parsers.SimpleRecognizerCorrect Fiat.Parsers.RecognizerPreOptimized Fiat.Parsers.Splitters.RDPList Fiat.Parsers.GenericRecognizerOptimized Fiat.Parsers.GenericRecognizerOptimizedTactics Fiat.Common