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

fix(tests/lean): adjust tests to reflect changes in the pretty printer

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-10 11:10:38 -07:00
parent 207e8e86da
commit 8f711873a0
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/bad_eqns.lean.expected.out
View file

@ -3,7 +3,7 @@ bad_eqns.lean:4:10: error: invalid argument, it is not a constructor, variable,
in the following equation left-hand-side
foo1 (0 + x)
bad_eqns.lean:8:10: error: invalid equation left-hand-side, variable 'y' only occurs in inaccessible terms in the following equation left-hand-side
foo2 x y
foo2 x ⌞y⌟
bad_eqns.lean:10:11: error: invalid recursive equations for 'foo3', inconsistent use of inaccessible term annotation, in some equations a pattern is a constructor, and in another it is an inaccessible term
bad_eqns.lean:21:11: error: mutual recursion is not needed when defining non-recursive functions
bad_eqns.lean:34:11: error: invalid recursive equations, failed to find recursive arguments that are structurally smaller (possible solution: use well-founded recursion)

2
tests/lean/error_loc_bug.lean.expected.out
View file

@ -5,6 +5,6 @@ term
has type
Γ ⊢ A ∨ B
but is expected to have type
Γ ⊢ A ∧ B
Γ ⊢ ⌞A ∧ B⌟
The following identifier(s) are introduced as free variables by the left-hand-side of the equation:
Γ A B Δ H Hs