From c2df664c3933752d5f4b05ea6d0cf6756575905e Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Mon, 29 May 2017 14:55:05 -0400
Subject: [PATCH] feat(library/init/meta/tactic): make tactics that introduce a
 local constant return the expr

---
 library/init/meta/interactive.lean | 18 ++++++++++++------
 library/init/meta/tactic.lean      | 20 ++++++++++----------
 2 files changed, 22 insertions(+), 16 deletions(-)

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 11788b2f9a..a91faa0ee1 100644
--- a/library/init/meta/interactive.lean
+++ b/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
 
 /--
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 23fae587cd..ac6d67c3e2 100644
--- a/library/init/meta/tactic.lean
+++ b/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