feat(library/init/meta/interactive): add sorry interactive tactic (alias for admit).

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.

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.
 -/

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
 }

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

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

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