From 9f3109689213c682d2deebca441c60011e4fbbac Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 15 Jun 2017 00:52:00 -0400
Subject: [PATCH] refactor(init/meta/interactive): rename pose -> define

---
 library/data/bitvec.lean               |  2 +-
 library/init/meta/interactive.lean     |  2 +-
 library/init/meta/smt/interactive.lean | 60 ++++++++++++++------------
 3 files changed, 34 insertions(+), 30 deletions(-)

diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean
index 2092ee44b0..5323de51d7 100644
--- a/library/data/bitvec.lean
+++ b/library/data/bitvec.lean
@@ -165,7 +165,7 @@ section conversion
     simp [bits_to_nat_to_list], clear P,
     unfold bits_to_nat list.foldl,
       -- the next 4 lines generalize the accumulator of foldl
-    pose x := 0,
+    define x := 0,
     change _ = add_lsb x b + _,
     generalize 0 y,
     revert x, simp,
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index c86a02d319..dd12bfc000 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -469,7 +469,7 @@ match q₁, q₂ with
   tactic.assert h e
 end >> skip
 
-meta def pose (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
+meta def define (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
 let h := h.get_or_else `this in
 match q₁, q₂ with
 | some e, some p := do
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index 33c8846603..c3a184f4f2 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -77,35 +77,39 @@ tactic.interactive.change q none (loc.ns [])
 meta def exact (q : parse texpr) : smt_tactic unit :=
 tactic.interactive.exact q
 
-meta def assert (h : parse ident) (q : parse $ tk ":" *> texpr) : smt_tactic unit :=
-do e ← tactic.to_expr_strict q,
-   smt_tactic.assert h e
+meta def note (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : smt_tactic unit :=
+let h := h.get_or_else `this in
+match q₁, q₂ with
+| some e, some p := do
+  t ← tactic.to_expr e,
+  v ← tactic.to_expr ``(%%p : %%t),
+  smt_tactic.assertv h t v
+| none, some p := do
+  p ← tactic.to_expr p,
+  smt_tactic.note h none p
+| some e, none := tactic.to_expr e >>= smt_tactic.assert h
+| none, none := do
+  u ← tactic.mk_meta_univ,
+  e ← tactic.mk_meta_var (expr.sort u),
+  smt_tactic.assert h e
+end >> return ()
 
-meta def define (h : parse ident) (q : parse $ tk ":" *> texpr) : smt_tactic unit :=
-do e ← tactic.to_expr_strict q,
-   smt_tactic.define h e
-
-meta def note (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ tk ":=" *> texpr) : smt_tactic unit :=
-match q₁ with
-| some e := do
-  t ← tactic.to_expr_strict e,
-  v ← tactic.to_expr_strict ``(%%q₂ : %%t),
-  smt_tactic.assertv (h.get_or_else `this) t v
-| none := do
-  p ← tactic.to_expr_strict q₂,
-  smt_tactic.note (h.get_or_else `this) none p
-end
-
-meta def pose (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ tk ":=" *> texpr) : smt_tactic unit :=
-match q₁ with
-| some e := do
-  t ← tactic.to_expr_strict e,
-  v ← tactic.to_expr_strict ``(%%q₂ : %%t),
-  smt_tactic.definev (h.get_or_else `this) t v
-| none := do
-  p ← tactic.to_expr_strict q₂,
-  smt_tactic.pose (h.get_or_else `this) none p
-end
+meta def define (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : smt_tactic unit :=
+let h := h.get_or_else `this in
+match q₁, q₂ with
+| some e, some p := do
+  t ← tactic.to_expr e,
+  v ← tactic.to_expr ``(%%p : %%t),
+  smt_tactic.definev h t v
+| none, some p := do
+  p ← tactic.to_expr p,
+  smt_tactic.pose h none p
+| some e, none := tactic.to_expr e >>= smt_tactic.define h
+| none, none := do
+  u ← tactic.mk_meta_univ,
+  e ← tactic.mk_meta_var (expr.sort u),
+  smt_tactic.define h e
+end >> return ()
 
 meta def add_fact (q : parse texpr) : smt_tactic unit :=
 do h ← tactic.get_unused_name `h none,