fact: Definition intro_base {A B} (var : name) (t : A -> gtactic B) : gtactic B := fun g => mmatch g return M (mlist (B *m goal gs_any)) with | [? s B (def: B) P e] Metavar s (let x := def in P x) e =n> eqBA <- M.unify_or_fail UniCoq B A; M.nu var (mSome def) (fun x=> let Px := reduce (RedWhd [rl:RedBeta]) (P x) in e' <- M.sorted_evar _ Px; nG <- M.abs_let (P:=P) x def e'; exact nG g;; let x := reduce (RedWhd [rl:RedMatch]) (match eqBA with meq_refl => x end) in t x (Metavar s _ e') >>= let_close_goals x) | [? (s:Sort) (P:_->s) e] Metavar s (ForAll (fun x:A => P x)) e =u> M.nu var mNone (fun x=> let Px := reduce (RedWhd [rl:RedBeta]) (P x) in e' <- M.sorted_evar _ Px; nG <- M.abs_fun (P:=P) x e'; exact nG g;; t x (Metavar s Px e') >>= close_goals x) | [? (s:Sort) B (P:_->s) e] Metavar s (ForAll (fun x:A => P x)) e =u> mtry M.unify_or_fail UniCoq A B;; M.failwith "intros: impossible" with _ => M.raise IntroDifferentType end | _ => M.raise NotAProduct end.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic Sorts MTeleMatch) Strings.String NArith.BinNat NArith.BinNatDef