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

fix(tests): fix tests

Browse source
This commit is contained in:
Mario Carneiro 2017-07-20 22:51:42 +01:00 • committed by Leonardo de Moura
parent 97a01d25fd
commit 94ecc3292f
2 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/andthen_focus_error_message.lean.expected.out
View file

@ -8,11 +8,9 @@ a b c : ℕ
⊢ b = b
andthen_focus_error_message.lean:16:14: error: focus tactic failed, insufficient number of tactics
state:
no goals
a : ℕ
⊢ a = a
andthen_focus_error_message.lean:22:14: error: focus tactic failed, insufficient number of tactics
state:
a : ℕ
⊢ a = a
a : ℕ
⊢ a = a

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

@ -1,4 +1,4 @@
{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":4,"severity":"error","text":"focus tactic failed, insufficient number of tactics\nstate:\nb c : ℕ,\na_2 : b = 0\n⊢ b = 0"}],"response":"all_messages"}
{"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":{"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":{"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}