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

fix(tests/lean): adjust tests expected output

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-13 12:35:14 -07:00
parent e5a36467dd
commit e778e3faec
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/t3.lean.expected.out
View file

@ -10,7 +10,7 @@ Type
Type
Type
t3.lean:26:10: error: invalid namespace declaration, atomic identifier expected
t3.lean:27:1: error: invalid declaration name 'full.name.U', identifier must be atomic
t3.lean:27:0: error: invalid declaration name 'full.name.U', identifier must be atomic
Type
Type
t3.lean:35:2: error: universe level alias 'u' shadows existing global universe level

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

@ -1,3 +1,3 @@
add a (mul b a) : N
t9.lean:16:8: error: invalid expression
t9.lean:16:7: error: invalid expression
add a (mul b a) : N