feat(lift): check whether target is proposition (#1767)

* feat(lift): check whether target is proposition * simplify
leanprover-community · Dec 4, 2019 · 71247eb · 71247eb
1 parent c1105de
commit 71247eb
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git a/src/tactic/lift.lean b/src/tactic/lift.lean
@@ -79,6 +79,8 @@ if h_some : h.is_some then
   -/
 meta def lift (p : pexpr) (t : pexpr) (h : option pexpr) (n : list name) : tactic unit :=
 do
+  propositional_goal <|>
+    fail "lift tactic failed. Tactic is only applicable when the target is a proposition.",
   e ← i_to_expr p,
   old_tp ← infer_type e,
   new_tp ← i_to_expr t,

diff --git a/test/tactics.lean b/test/tactics.lean
@@ -304,6 +304,13 @@ begin
   trivial
 end
 
+example (n : ℤ) : ℕ :=
+begin
+  success_if_fail_with_msg {lift n to ℕ}
+    "lift tactic failed. Tactic is only applicable when the target is a proposition.",
+  exact 0
+end
+
 end lift
 
 private meta def get_exception_message (t : lean.parser unit) : lean.parser string