fact: Definition parse_item' (str_matches_nonterminal : nonterminal_carrierT -> parse_nt_T) (offset : nat) (len : nat) (it : item Char) : parse_item_T := match it with | Terminal P => if Nat.eqb len 1 && char_at_matches offset str P then ret_Terminal_true (unsafe_get offset str) else ret_Terminal_false (unsafe_get offset str) | NonTerminal nt => if is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt) then ret_NonTerminal_true nt (str_matches_nonterminal (of_nonterminal nt)) else ret_NonTerminal_false nt end%bool.
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