diff --git a/tests/lean/abbrev1.lean b/tests/lean/abbrev1.lean
new file mode 100644
index 000000000..b2f739efe
--- /dev/null
+++ b/tests/lean/abbrev1.lean
@@ -0,0 +1,19 @@
+open nat
+
+abbreviation foo  : Π (A : Type), nat := λ a, 2 + 3
+
+definition tst := foo nat
+
+set_option pp.abbreviations false
+
+print definition tst
+
+set_option pp.abbreviations true
+
+print definition tst
+
+abbreviation id [parsing-only] {A : Type} (a : A) := a
+
+definition tst1 := id 10
+
+print definition tst1
diff --git a/tests/lean/abbrev1.lean.expected.out b/tests/lean/abbrev1.lean.expected.out
new file mode 100644
index 000000000..6d1aa39e2
--- /dev/null
+++ b/tests/lean/abbrev1.lean.expected.out
@@ -0,0 +1,3 @@
+(λ (a : Type₁), 2 + 3) ℕ
+foo ℕ
+(λ (A : Type₁) (a : A), a) num 10