From c3d4a9456edbb781840d0b64f9e2dca4fd8db21d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 11 Jan 2018 16:54:10 -0800
Subject: [PATCH] feat(library/init/meta/interactive): add `sorry` interactive
 tactic (alias for `admit`).

---
 doc/changes.md                          | 2 ++
 library/init/meta/interactive.lean      | 5 +++++
 tests/lean/bad_error5.lean              | 1 -
 tests/lean/bad_error5.lean.expected.out | 6 +-----
 tests/lean/vm_sorry.lean                | 1 +
 tests/lean/vm_sorry.lean.expected.out   | 1 +
 6 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/doc/changes.md b/doc/changes.md
index 3a7efa80b9..d14ae38f33 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -92,6 +92,8 @@ master branch (aka work in progress branch)
   ```
   The simplifier will try to use tactic `assumption` to synthesize parameter `h`.
 
+* Add interactive `sorry` tactic (alias for `admit`).
+
 *Changes*
 
 * Replace `inout` modifier in type class declarations with `out_param` modifier.
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 93fdca801d..0ce99b63f6 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -813,6 +813,11 @@ Closes the main goal using `sorry`.
 -/
 meta def admit : tactic unit := tactic.admit
 
+/--
+Closes the main goal using `sorry`.
+-/
+meta def «sorry» : tactic unit := tactic.admit
+
 /--
 The contradiction tactic attempts to find in the current local context a hypothesis that is equivalent to an empty inductive type (e.g. `false`), a hypothesis of the form `c_1 ... = c_2 ...` where `c_1` and `c_2` are distinct constructors, or two contradictory hypotheses.
 -/
diff --git a/tests/lean/bad_error5.lean b/tests/lean/bad_error5.lean
index c80839b5b1..13a5f18fe5 100644
--- a/tests/lean/bad_error5.lean
+++ b/tests/lean/bad_error5.lean
@@ -9,6 +9,5 @@ structure U (c: S) (A : c^.α)
 definition V (c : S) : S :=
 {
   α := T c,
-  -- code generation error should be shown on tactic
   β := by sorry
 }
diff --git a/tests/lean/bad_error5.lean.expected.out b/tests/lean/bad_error5.lean.expected.out
index 49f59c49fa..29529c20d9 100644
--- a/tests/lean/bad_error5.lean.expected.out
+++ b/tests/lean/bad_error5.lean.expected.out
@@ -1,5 +1 @@
-bad_error5.lean:13:10: error: don't know how to synthesize placeholder
-context:
-c : S
-⊢ Type ?
-bad_error5.lean:13:10: error: _interaction._lambda_3: trying to evaluate sorry
+bad_error5.lean:9:0: warning: declaration 'V' uses sorry
diff --git a/tests/lean/vm_sorry.lean b/tests/lean/vm_sorry.lean
index a72a4c8f15..93a1d933cc 100644
--- a/tests/lean/vm_sorry.lean
+++ b/tests/lean/vm_sorry.lean
@@ -18,3 +18,4 @@ run_cmd (do v ← to_expr ``(half_baked ff) >>= whnf,
 example : 0 = 1 := by admit
 example : 0 = 1 := by mk_sorry >>= exact
 example : 0 = 1 := by exact sorry
+example : 0 = 1 := by sorry
diff --git a/tests/lean/vm_sorry.lean.expected.out b/tests/lean/vm_sorry.lean.expected.out
index 4d538597ad..3a2cc58146 100644
--- a/tests/lean/vm_sorry.lean.expected.out
+++ b/tests/lean/vm_sorry.lean.expected.out
@@ -6,3 +6,4 @@ vm_sorry.lean:12:0: error: undefined
 vm_sorry.lean:18:0: warning: declaration '[anonymous]' uses sorry
 vm_sorry.lean:19:0: warning: declaration '[anonymous]' uses sorry
 vm_sorry.lean:20:0: warning: declaration '[anonymous]' uses sorry
+vm_sorry.lean:21:0: warning: declaration '[anonymous]' uses sorry