fact: Fixpoint inferHead' (s:Ast.term) (revArg R: list Ast.term) : TemplateMonad (L.term * list Ast.term) := s'0 <- tmEval cbn (if forallb (fun _ => false) revArg then s else Ast.tApp s (rev revArg));; s' <- tmUnquote s'0;; s'' <- tmEval cbn (my_projT2 s');; res <- tmInferInstance None (extracted (A:=my_projT1 s') s'');; match res with my_Some s'' => ret (s'',R) | my_None => let doSplit := match R with | [] => false | r :: R => if closedn 0 r then true else false end in match doSplit,R with true,r::R => inferHead' s (r::revArg) R | _,_ => let lhs := string_of_term s'0 in let rhs := string_of_list string_of_term R in tmMsg "More readable: initial segment:";;tmPrint s'';;tmMsg "With remainder:";;tmPrint R;; tmFail ("Could not extract in inferHead (moreReadable version in *coq*): could not infer any instance for initial segment of " ++lhs ++ " with further arguments "++ rhs) end end.
imports: Ascii String Undecidability.L(Util.L_facts) MetaCoq(Template.All Template.Checker) Undecidability.Shared.Libs.PSL.Base MetaCoq.Utils.bytestring