fact: Fixpoint size_of_maybe_empty_productions {pats} (p : maybe_empty_productions G valid pats) : nat := match p with | MaybeEmptyHead _ _ p' => S (size_of_maybe_empty_production p') | MaybeEmptyTail _ _ p' => S (size_of_maybe_empty_productions p') end with size_of_maybe_empty_production {pat} (p : maybe_empty_production G valid pat) : nat := match p with | MaybeEmptyProductionNil => 0 | MaybeEmptyProductionCons _ _ p0 p1 => S (size_of_maybe_empty_item' (@size_of_maybe_empty_productions) p0 + size_of_maybe_empty_production p1) end.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.Reachable.MaybeEmpty.Core Fiat.Parsers.BaseTypes