diff --git a/tests/lean/errors.lean b/tests/lean/errors.lean
new file mode 100644
index 0000000000..591cf06b18
--- /dev/null
+++ b/tests/lean/errors.lean
@@ -0,0 +1,38 @@
+namespace foo
+
+definition tst1 : nat → nat → nat :=
+a + b  -- ERROR
+
+check tst1
+
+definition tst2 : nat → nat → nat :=
+begin
+  intro a,
+  intro b,
+  cases add wth (a, b), -- ERROR
+  exact a,
+  exact b,
+end
+
+  section
+    parameter A : Type
+    definition tst3 : A → A → A :=
+    begin
+      intro a,
+      apply b, -- ERROR
+      exact a
+    end
+
+    check tst3
+  end
+
+end foo
+
+open nat
+
+definition bla : nat :=
+foo.tst1 0 0 + foo.tst2 0 0 + foo.tst3 nat 1 1
+
+check foo.tst1
+check foo.tst2
+check foo.tst3
diff --git a/tests/lean/errors.lean.expected.out b/tests/lean/errors.lean.expected.out
new file mode 100644
index 0000000000..51eb795a8b
--- /dev/null
+++ b/tests/lean/errors.lean.expected.out
@@ -0,0 +1,8 @@
+errors.lean:4:0: error: unknown identifier 'a'
+tst1 : nat → nat → nat
+errors.lean:12:12: error: invalid tactic expression
+errors.lean:22:12: error: unknown identifier 'b'
+tst3 A : A → A → A
+foo.tst1 : ℕ → ℕ → ℕ
+foo.tst2 : ℕ → ℕ → ℕ
+foo.tst3 : Π (A : Type), A → A → A