fact: Definition evaluate_ritem' (evaluate_productions : simple_parse_of Char -> rproductions_with_actions Char T -> option T) (pit : simple_parse_of_item Char) (it : Reflective.ritem Char) : option match it with | Reflective.RTerminal _ => Char | Reflective.RNonTerminal _ => T end := match pit, it as x return option match pit with | SimpleParseTerminal _ => Char | SimpleParseNonTerminal _ _ => T end -> option match x with | Reflective.RTerminal _ => Char | Reflective.RNonTerminal _ => T end with | SimpleParseTerminal ch, Reflective.RTerminal ch' => fun x => x | SimpleParseNonTerminal nt p', Reflective.RNonTerminal nt' => if Equality.string_beq nt nt' then fun x => x else fun _ => impossible | SimpleParseTerminal _, Reflective.RNonTerminal _ | SimpleParseNonTerminal _ _, Reflective.RTerminal _ => fun _ => None end (evaluate_item' evaluate_productions pit).
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericRecognizer