diff --git a/tests/lean/errmsg1.lean b/tests/lean/errmsg1.lean
new file mode 100644
index 000000000..b1502b5c3
--- /dev/null
+++ b/tests/lean/errmsg1.lean
@@ -0,0 +1,8 @@
+Eval fun x, x
+Show fun x, x
+
+Check fun x, x
+Theorem T (A : Type) (x : A) : Pi (y : A), A
+:= _.
+
+Theorem T (x : _) : x = x := Refl x.
diff --git a/tests/lean/errmsg1.lean.expected.out b/tests/lean/errmsg1.lean.expected.out
new file mode 100644
index 000000000..9c0be009d
--- /dev/null
+++ b/tests/lean/errmsg1.lean.expected.out
@@ -0,0 +1,10 @@
+  Set: pp::colors
+  Set: pp::unicode
+λ x : ?M::0, x
+λ x : ?M::0, x
+Error (line: 4, pos: 10) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::0, type:
+(Type U)
+Error (line: 6, pos: 3) failed to synthesize metavar, its type is not a proposition, metavariable: ?M::0, type:
+A : Type, x : A ⊢ A → A
+Error (line: 8, pos: 34) invalid definition, type still contains metavariables after elaboration, metavariable: ?M::3, type:
+(Type U)