From 0b335230d71253c9be5cc6e81268ba7f89ca3298 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 10 Jun 2015 16:33:27 -0700
Subject: [PATCH] test(tests/lean): add test for eta at postprocessing

---
 tests/lean/eta_decls.lean              | 9 +++++++++
 tests/lean/eta_decls.lean.expected.out | 4 ++++
 2 files changed, 13 insertions(+)
 create mode 100644 tests/lean/eta_decls.lean
 create mode 100644 tests/lean/eta_decls.lean.expected.out

diff --git a/tests/lean/eta_decls.lean b/tests/lean/eta_decls.lean
new file mode 100644
index 000000000..51fd8120a
--- /dev/null
+++ b/tests/lean/eta_decls.lean
@@ -0,0 +1,9 @@
+import data.finset
+open finset
+
+set_option pp.implicit true
+set_option pp.notation false
+set_option pp.beta false
+
+check @to_set_union
+check @to_set_empty
diff --git a/tests/lean/eta_decls.lean.expected.out b/tests/lean/eta_decls.lean.expected.out
new file mode 100644
index 000000000..c7a7ad6dc
--- /dev/null
+++ b/tests/lean/eta_decls.lean.expected.out
@@ -0,0 +1,4 @@
+to_set_union :
+  ∀ {A : Type} [deceq : decidable_eq A] (s t : finset A),
+    @eq (set A) (@ts A (@union A deceq s t)) (@set.union A (@ts A s) (@ts A t))
+to_set_empty : ∀ {A : Type}, @eq (set A) (@ts A (@empty A)) (@set.empty A)