diff --git a/tests/lean/kernel_ex1.lean b/tests/lean/kernel_ex1.lean
new file mode 100644
index 000000000..85cb8b023
--- /dev/null
+++ b/tests/lean/kernel_ex1.lean
@@ -0,0 +1,6 @@
+variable N : Type
+variable a : N
+check fun x : a, x
+check a a
+variable f : N -> N
+check f (fun x : N, x)
\ No newline at end of file
diff --git a/tests/lean/kernel_ex1.lean.expected.out b/tests/lean/kernel_ex1.lean.expected.out
new file mode 100644
index 000000000..be5da0b38
--- /dev/null
+++ b/tests/lean/kernel_ex1.lean.expected.out
@@ -0,0 +1,15 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: N
+  Assumed: a
+Error (line: 3, pos: 14) type expected, got
+    a
+Error (line: 4, pos: 6) function expected at
+    a a
+  Assumed: f
+Error (line: 6, pos: 6) type mismatch at application
+    f (λ x : N, x)
+Function type:
+    N → N
+Argument type:
+    (λ x : N, x) : N → N