test(tests/lean): add more tests for error messages

This commit is contained in:
Leonardo de Moura 2015-02-01 20:02:49 -08:00
parent 3f37c0e739
commit ed85ac254a
6 changed files with 17 additions and 0 deletions

View file

@ -0,0 +1 @@
namespace _root_

View file

@ -0,0 +1 @@
bad_namespace.lean:1:10: error: invalid namespace name, '_root_' is reserved

3
tests/lean/bad_open.lean Normal file
View file

@ -0,0 +1,3 @@
open "nat"
open [classes] "nat"

View file

@ -0,0 +1,2 @@
bad_open.lean:1:5: error: invalid 'open/export' command, identifier expected
bad_open.lean:3:15: error: invalid 'open/export' command, identifier expected

View file

@ -0,0 +1,7 @@
constant boo : nat
print definition boo
print 2
print fields nat

View file

@ -0,0 +1,3 @@
bad_print.lean:3:17: error: invalid 'print definition', 'boo' is not a definition
bad_print.lean:5:6: error: invalid print command
bad_print.lean:7:13: error: invalid 'print fields' command, 'nat' is not a structure