fact: Fixpoint size_of_parse {str pats} (p : parse_of G str pats) : nat := @size_of_parse_step (@size_of_parse) (@size_of_parse_production) str pats p with size_of_parse_production {str pat} (p : parse_of_production G str pat) : nat := @size_of_parse_production_step (@size_of_parse) (@size_of_parse_production) str pat p.
imports: Coq.Strings.String Coq.Arith.Wf_nat Coq.Relations.Relation_Definitions Fiat.Parsers.ContextFreeGrammar.Core