michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean): test output to reflect recent changes

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-07 10:01:28 -07:00
parent ac24f19210
commit 5113f6b9d8
2 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -13,8 +13,12 @@ revert_fail.lean:6:0: error: failed to add declaration '14.0' to environment, va
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (A : Type) (n : nat) (v : …),
?M_1
revert_fail.lean:11:2: error: tactic failed
revert_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
proof state:
no goals
revert_fail.lean:12:0: error: don't know how to synthesize placeholder
n : nat
⊢ n = n
revert_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (n : nat),

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

@ -15,8 +15,12 @@ rewrite_fail.lean:6:0: error: failed to add declaration '14.0' to environment, v
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a b : ℕ) (Ha : …) (Hb : …),
?M_1
rewrite_fail.lean:11:2: error: tactic failed
rewrite_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
proof state:
no goals
rewrite_fail.lean:12:0: error: don't know how to synthesize placeholder
a : ℕ
⊢ a = a
rewrite_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
λ (a : ℕ),