From 5bdc54d34473d9fc10dea2cf28a40f6fb584aeb8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Mar 2020 08:35:34 -0800
Subject: [PATCH] test: unifier

---
 tests/lean/run/etaFirst.lean | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 tests/lean/run/etaFirst.lean

diff --git a/tests/lean/run/etaFirst.lean b/tests/lean/run/etaFirst.lean
new file mode 100644
index 0000000000..7742d34d12
--- /dev/null
+++ b/tests/lean/run/etaFirst.lean
@@ -0,0 +1,35 @@
+-- The following fails in the old elaborator
+-- theorem tst1 : (fun a b => Nat.add a b) = Nat.add :=
+-- Eq.refl (fun a b => Nat.add a b)
+
+new_frontend
+
+theorem tst2 : (fun a b => Nat.add a b) = Nat.add :=
+Eq.refl (fun a b => Nat.add a b)
+
+theorem tst3 : (fun a b => Nat.add a b) = Nat.add :=
+rfl
+
+theorem tst4 : Nat.add = (fun a b => Nat.add a b) :=
+rfl
+
+theorem tst5 : Nat.add = (fun (a b : Nat) => a + b) :=
+rfl
+
+theorem tst6 : Nat.add = (· + ·) :=
+rfl
+
+theorem tst7 : (· + ·) = Nat.add :=
+rfl
+
+theorem tst8 : (· + ·) = @HasAdd.add Nat _ :=
+rfl
+
+theorem tst9 : (Nat.add · ·) = @HasAdd.add Nat _ :=
+rfl
+
+axiom p    : (Nat → Nat → Nat) → Prop
+axiom pAdd : p Nat.add
+
+theorem tst10 : p (fun a b => Nat.add a b) :=
+pAdd