fact: Fixpoint fuse_production (res : list (Char + T)) (pat : rproduction_with_action Char T) : option T := match res, projT1 pat as pat' return action_of_rproduction T pat' -> option T with | nil, nil => @Some _ | inl v :: res', Reflective.RTerminal _ :: pats' | inr v :: res', Reflective.RNonTerminal _ :: pats' => fun f => @fuse_production res' (existT _ pats' (f v)) | inl _ :: _, Reflective.RNonTerminal _ :: _ | inr _ :: _, Reflective.RTerminal _ :: _ | nil, _::_ | _::_, nil => fun _ => None end%list (projT2 pat).
imports: Coq.Strings.String Fiat.Parsers.GenericBaseTypes Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations