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

chore(tests/lean): fix tests output

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-17 09:56:57 -07:00
parent c8c43a866b
commit 7f810d3db5
3 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,8 +1,14 @@
f a b : A
f a b : A
expr ↣ _Fun : expr.app
string ↣ name : mk_simple_name
nat ↣ bool : foo
expr ↣ [fun-class] : expr.app
expr ↣ _Fun : expr.app
string ↣ name : mk_simple_name
expr ↣ [fun-class] : expr.app
10 : ?M_1
local_notation_bug.lean:22:8: error: invalid expression
expr ↣ _Fun : expr.app
string ↣ name : mk_simple_name
expr ↣ [fun-class] : expr.app

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

@ -1,5 +1,7 @@
expr ↣ _Fun : expr.app
string ↣ name : mk_simple_name
C ↣ _Fun : f
expr ↣ [fun-class] : expr.app
C ↣ [fun-class] : f
c
c trivial

4
tests/lean/sec2.lean.expected.out
View file

@ -1,5 +1,7 @@
expr ↣ _Fun : expr.app
string ↣ name : mk_simple_name
A ↣ B : f
expr ↣ [fun-class] : expr.app
g a : B
sec2.lean:13:6: error: type mismatch at application
g a
@ -9,7 +11,9 @@ has type
A
but is expected to have type
B
expr ↣ _Fun : expr.app
string ↣ name : mk_simple_name
A ↣ B : f
expr ↣ [fun-class] : expr.app
g a : B
g a : B