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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-13 12:36:33 -07:00
parent 667f2ed601
commit fb6dfa4af2
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,5 +1,5 @@
Bla.foo=="world" : Bool
private.lean:14:8: error: private declaration 'Bla.foo' has already been declared
private.lean:14:12: error: private declaration 'Bla.foo' has already been declared
foo==0 : Bool
Bla.foo : String
Boo.Bla.boo=="world" : Bool
@ -9,5 +9,5 @@ Boo.boo==100 : Bool
Boo.Bla.boo=="world" : Bool
Boo.boo==100 : Bool
Nat.mul10 x : Nat
private.lean:65:8: error: a non-private declaration 'y' has already been declared
private.lean:68:0: error: a private declaration 'z' has already been declared
private.lean:65:12: error: a non-private declaration 'y' has already been declared
private.lean:68:4: error: a private declaration 'z' has already been declared