fact: Definition abstract_from_term_dep {A} {B} (x:A) (y:B) (D : B -> Type) (ok : forall C : A -> B, M (D (C x))) (fail : M (D y)) : M (D y) := mtry '(m: _, gs) <- M.call_ltac Propₛ (A:=wrapper y) "Mssrpattern" [m:Dyn x]; mmatch gs with | [? y (f:A->B) t] [m: AnyMetavar Propₛ (let z := y in wrapper (f z)) t] =u> M.raise (@Backtrack A B y f) | _ => M.print_term gs;; M.failwith "abstract_from_sort: mmatch goal not ground" end with | [#] @Backtrack A B x | f =u> o <- M.unify (f x) (y) UniCoq; match o with | mSome eq => match eq in _ =m= B return M (D B) with | meq_refl => ok f end | mNone => M.failwith "abstract_from_sort: terms not unifiable" end | ExceptionNotGround => M.failwith "abstract_from_sort: backtrack" | [?s] Failure s => M.raise (Failure s) | [?s] LtacError s => fail end.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic intf.Sorts) Strings.String NArith.BinNat NArith.BinNatDef