From f9832fb89f67d3e3fd949c3c2fd329995b937b63 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Feb 2015 18:28:48 -0800
Subject: [PATCH] test(tests/lean/abbrev1): add test for abbreviation command

---
 tests/lean/abbrev1.lean              | 19 +++++++++++++++++++
 tests/lean/abbrev1.lean.expected.out |  3 +++
 2 files changed, 22 insertions(+)
 create mode 100644 tests/lean/abbrev1.lean
 create mode 100644 tests/lean/abbrev1.lean.expected.out

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