From 87f2ec08ad2396cfa129011eaf46c48ba01ef416 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 4 Sep 2017 13:04:36 -0400 Subject: [PATCH] feat(init/meta/interactive): suffices tactic Just a simple manipulation of the `have` tactic, but it allows the use of `suffices h : T, from p,` in tactic mode. --- library/init/meta/interactive.lean | 8 ++++++++ tests/lean/keyword_tactics.lean | 5 +++++ tests/lean/keyword_tactics.lean.expected.out | 4 ++++ 3 files changed, 17 insertions(+) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 0c0c2d72cd..d751964aaa 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -644,6 +644,14 @@ match q₁, q₂ with tactic.define h e end >> skip +/-- +This tactic applies to any goal. `suffices h : T` is the same as `have h : T, tactic.swap`. +It mirrors the `suffices` term in term mode. This tactic can be followed by `from P` to +prove the subgoal. +-/ +meta def «suffices» (h : parse ident?) (t : parse (tk ":" *> texpr)?) : tactic unit := +«have» h t none >> tactic.swap + /-- This tactic displays the current state in the tracing buffer. diff --git a/tests/lean/keyword_tactics.lean b/tests/lean/keyword_tactics.lean index 0e3b549cfc..008d87b722 100644 --- a/tests/lean/keyword_tactics.lean +++ b/tests/lean/keyword_tactics.lean @@ -44,3 +44,8 @@ example (f : ℕ → ℕ) : bool := begin have : ℕ, by apply f, end + +example (f : ℕ → ℕ) : bool := +begin + suffices: ℕ → bool, from this 0, +end diff --git a/tests/lean/keyword_tactics.lean.expected.out b/tests/lean/keyword_tactics.lean.expected.out index b089175ea0..2aef63a644 100644 --- a/tests/lean/keyword_tactics.lean.expected.out +++ b/tests/lean/keyword_tactics.lean.expected.out @@ -8,3 +8,7 @@ keyword_tactics.lean:45:15: error: solve1 tactic failed, focused goal has not be state: f : ℕ → ℕ ⊢ ℕ +keyword_tactics.lean:51:0: error: tactic failed, there are unsolved goals +state: +f : ℕ → ℕ +⊢ ℕ → bool