diff --git a/tests/lean/parser_error_recovery.lean b/tests/lean/parser_error_recovery.lean
new file mode 100644
index 0000000000..e3bcd764f4
--- /dev/null
+++ b/tests/lean/parser_error_recovery.lean
@@ -0,0 +1,21 @@
+/- unknown identifiers -/
+
+def f1 : ℕ → ℕ
+| 42 := 9000
+| arg := ag
+
+#eval f1 42 -- OK (prints 9000)
+
+/- incomplete structure instances -/
+
+def f2 : ℕ × ℕ := { fst := 9000, sn}
+
+#reduce f2.fst -- OK (prints 9000)
+
+/- incomplete if-then-else -/
+
+def f3 (x : ℕ) : ℕ :=
+(if x ≥ 42 then 9000)
+                 -- ^ missing else reported here
+
+#eval f3 42 -- OK (prints 9000)
\ No newline at end of file
diff --git a/tests/lean/parser_error_recovery.lean.expected.out b/tests/lean/parser_error_recovery.lean.expected.out
new file mode 100644
index 0000000000..07f1ca5fc6
--- /dev/null
+++ b/tests/lean/parser_error_recovery.lean.expected.out
@@ -0,0 +1,10 @@
+parser_error_recovery.lean:5:9: error: unknown identifier 'ag'
+parser_error_recovery.lean:3:0: warning: declaration 'f1' uses sorry
+9000
+parser_error_recovery.lean:11:35: error: invalid structure instance, ':=' expected
+parser_error_recovery.lean:11:18: error: invalid structure value { ... }, field 'snd' was not provided
+parser_error_recovery.lean:11:18: error: invalid structure value { ... }, 'sn' is not a field of structure 'prod'
+9000
+parser_error_recovery.lean:18:20: error: invalid 'if-then-else' expression, 'else' expected
+parser_error_recovery.lean:17:0: warning: declaration 'f3' uses sorry
+9000