fact: Definition size_of_parse_production_step {str pat} (p : parse_of_production G str pat) : nat := match p with | ParseProductionNil _ => 0 | ParseProductionCons _ _ _ p' p'' => S (size_of_parse_item' (@size_of_parse) p' + @size_of_parse_production _ _ p'') end.
imports: Coq.Strings.String Coq.Arith.Wf_nat Coq.Relations.Relation_Definitions Fiat.Parsers.ContextFreeGrammar.Core