max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(interactive): fix focus tactic.

Browse source 
Previously it would fail if there was more than one goal.
This commit is contained in:
Floris van Doorn 2017-10-29 14:26:06 -04:00 • committed by Leonardo de Moura
parent f847622c93
commit 52ee29cb48
2 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/interactive.lean
View file

@ -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,

3
tests/lean/interactive/focus.lean.expected.out
View file

@ -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}