fact: Definition simple_parse_of_correct_step (str : String) (pats : productions Char) (t : simple_parse_of) : Prop := match t with | SimpleParseHead t' => match pats with | nil => False | pat'::pats' => simple_parse_of_production_correct str pat' t' end | SimpleParseTail t' => match pats with | nil => False | pat'::pats' => simple_parse_of_correct str pats' t' end end.
imports: Coq.Lists.List Fiat.Parsers.ContextFreeGrammar.Core