feat(library/init/meta/tactic): make tactics that introduce a local constant return the expr

library/init/meta/interactive.lean

@@ -535,11 +535,13 @@ The new subgoal becomes the main goal.
 -/
 meta def assert (h : parse ident) (q : parse $ tk ":" *> texpr) : tactic unit :=
 do e ← i_to_expr_strict q,
-   tactic.assert h e
+   tactic.assert h e,
+   return ()
 
 meta def define (h : parse ident) (q : parse $ tk ":" *> texpr) : tactic unit :=
 do e ← i_to_expr_strict q,
-   tactic.define h e
+   tactic.define h e,
+   return ()
 
 /--
 This tactic applies to any goal. `note h : T := p` adds a new hypothesis of name `h` and type `T` to the current goal if `p` a term of type `T`.
@@ -549,10 +551,12 @@ match q₁ with
 | some e := do
   t ← i_to_expr_strict e,
   v ← i_to_expr_strict ``(%%q₂ : %%t),
-  tactic.assertv (h.get_or_else `this) t v
+  tactic.assertv (h.get_or_else `this) t v,
+  return ()
 | none := do
   p ← i_to_expr_strict q₂,
-  tactic.note (h.get_or_else `this) none p
+  tactic.note (h.get_or_else `this) none p,
+  return ()
 end
 
 meta def pose (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ tk ":=" *> texpr) : tactic unit :=
@@ -560,10 +564,12 @@ match q₁ with
 | some e := do
   t ← i_to_expr_strict e,
   v ← i_to_expr_strict ``(%%q₂ : %%t),
-  tactic.definev (h.get_or_else `this) t v
+  tactic.definev (h.get_or_else `this) t v,
+  return ()
 | none := do
   p ← i_to_expr_strict q₂,
-  tactic.pose (h.get_or_else `this) none p
+  tactic.pose (h.get_or_else `this) none p,
+  return ()
 end
 
 /--

library/init/meta/tactic.lean

@@ -630,28 +630,28 @@ do gs ← get_goals,
    end
 
 /- (assert h t), adds a new goal for t, and the hypothesis (h : t) in the current goal. -/
-meta def assert (h : name) (t : expr) : tactic unit :=
-assert_core h t >> swap >> intro h >> swap
+meta def assert (h : name) (t : expr) : tactic expr :=
+do assert_core h t, swap, e ← intro h, swap, return e
 
 /- (assertv h t v), adds the hypothesis (h : t) in the current goal if v has type t. -/
-meta def assertv (h : name) (t : expr) (v : expr) : tactic unit :=
-assertv_core h t v >> intro h >> return ()
+meta def assertv (h : name) (t : expr) (v : expr) : tactic expr :=
+assertv_core h t v >> intro h
 
 /- (define h t), adds a new goal for t, and the hypothesis (h : t := ?M) in the current goal. -/
-meta def define  (h : name) (t : expr) : tactic unit :=
-define_core h t >> swap >> intro h >> swap
+meta def define  (h : name) (t : expr) : tactic expr :=
+do define_core h t, swap, e ← intro h, swap, return e
 
 /- (definev h t v), adds the hypothesis (h : t := v) in the current goal if v has type t. -/
-meta def definev (h : name) (t : expr) (v : expr) : tactic unit :=
-definev_core h t v >> intro h >> return ()
+meta def definev (h : name) (t : expr) (v : expr) : tactic expr :=
+definev_core h t v >> intro h
 
 /- Add (h : t := pr) to the current goal -/
-meta def pose (h : name) (t : option expr := none) (pr : expr) : tactic unit :=
+meta def pose (h : name) (t : option expr := none) (pr : expr) : tactic expr :=
 let dv := λt, definev h t pr in
 option.cases_on t (infer_type pr >>= dv) dv
 
 /- Add (h : t) to the current goal, given a proof (pr : t) -/
-meta def note (h : name) (t : option expr := none) (pr : expr) : tactic unit :=
+meta def note (h : name) (t : option expr := none) (pr : expr) : tactic expr :=
 let dv := λt, assertv h t pr in
 option.cases_on t (infer_type pr >>= dv) dv