diff --git a/tests/lean/bad_namespace.lean b/tests/lean/bad_namespace.lean
new file mode 100644
index 000000000..b5a3ba24b
--- /dev/null
+++ b/tests/lean/bad_namespace.lean
@@ -0,0 +1 @@
+namespace _root_
diff --git a/tests/lean/bad_namespace.lean.expected.out b/tests/lean/bad_namespace.lean.expected.out
new file mode 100644
index 000000000..0238afd21
--- /dev/null
+++ b/tests/lean/bad_namespace.lean.expected.out
@@ -0,0 +1 @@
+bad_namespace.lean:1:10: error: invalid namespace name, '_root_' is reserved
diff --git a/tests/lean/bad_open.lean b/tests/lean/bad_open.lean
new file mode 100644
index 000000000..254a12fea
--- /dev/null
+++ b/tests/lean/bad_open.lean
@@ -0,0 +1,3 @@
+open "nat"
+
+open [classes] "nat"
diff --git a/tests/lean/bad_open.lean.expected.out b/tests/lean/bad_open.lean.expected.out
new file mode 100644
index 000000000..ef40eec37
--- /dev/null
+++ b/tests/lean/bad_open.lean.expected.out
@@ -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
diff --git a/tests/lean/bad_print.lean b/tests/lean/bad_print.lean
new file mode 100644
index 000000000..d11b42dcb
--- /dev/null
+++ b/tests/lean/bad_print.lean
@@ -0,0 +1,7 @@
+constant boo : nat
+
+print definition boo
+
+print 2
+
+print fields nat
diff --git a/tests/lean/bad_print.lean.expected.out b/tests/lean/bad_print.lean.expected.out
new file mode 100644
index 000000000..4401d8835
--- /dev/null
+++ b/tests/lean/bad_print.lean.expected.out
@@ -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