fact: Definition parse_nonterminal_or_abort : forall (p : nat * nat) (valid : nonterminals_listT) (offset : nat) (len : nat), len <= fst p -> nonterminal_carrierT -> parse_nt_T := @Fix (nat * nat) _ (well_founded_prod_relation lt_wf lt_wf) _ (fun sl => @parse_nonterminal_step (fst sl) (snd sl)).
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Common.Wf