From 52ee29cb48750e3a73f7af4ae955b33da51599ac Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sun, 29 Oct 2017 14:26:06 -0400 Subject: [PATCH] fix(interactive): fix focus tactic. Previously it would fail if there was more than one goal. --- library/init/meta/interactive.lean | 2 +- tests/lean/interactive/focus.lean.expected.out | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 04091fc6b4..0e5835c227 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -640,7 +640,7 @@ tactic.any_goals `focus { t }` temporarily hides all goals other than the first, applies `t`, and then restores the other goals. It fails if there are no goals. -/ meta def focus (tac : itactic) : tactic unit := -tactic.focus [tac] +tactic.focus1 tac private meta def assume_core (n : name) (ty : pexpr) := do t ← target, diff --git a/tests/lean/interactive/focus.lean.expected.out b/tests/lean/interactive/focus.lean.expected.out index 7b474dcd02..0e09695851 100644 --- a/tests/lean/interactive/focus.lean.expected.out +++ b/tests/lean/interactive/focus.lean.expected.out @@ -1,5 +1,4 @@ -{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":4,"severity":"error","text":"focus tactic failed, insufficient number of tactics\nstate:\na b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ b = a"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"record":{"doc":"`focus { t }` temporarily hides all goals other than the first, applies `t`, and then restores the other goals. It fails if there are no goals.","source":,"state":"a b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ a = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":5} {"record":{"doc":"`focus { t }` temporarily hides all goals other than the first, applies `t`, and then restores the other goals. It fails if there are no goals.","source":,"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":7} -{"response":"ok","seq_num":9} +{"record":{"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0\n\na b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ b = a"},"response":"ok","seq_num":9}