From 4b2e4030234b0f8db0fe4a93400a4fadd5df9ece Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Jul 2014 12:17:38 -0700
Subject: [PATCH] test(tests/lean/run): add more tests sent by Cody

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/run/cody1.lean | 24 ++++++++++++++++++++++++
 tests/lean/run/cody2.lean | 23 +++++++++++++++++++++++
 2 files changed, 47 insertions(+)
 create mode 100644 tests/lean/run/cody1.lean
 create mode 100644 tests/lean/run/cody2.lean

diff --git a/tests/lean/run/cody1.lean b/tests/lean/run/cody1.lean
new file mode 100644
index 000000000..9db70c9f2
--- /dev/null
+++ b/tests/lean/run/cody1.lean
@@ -0,0 +1,24 @@
+import logic
+
+abbreviation subsets (P : Type) := P → Prop.
+
+section
+
+hypothesis A : Type.
+
+hypothesis r : A → subsets A.
+
+hypothesis i : subsets A → A.
+
+hypothesis retract {P : subsets A} {a : A} : r (i P) a = P a.
+
+definition delta (a:A) : Prop := ¬ (r a a).
+
+notation `δ` := delta.
+
+-- Crashes unifier!
+theorem false_aux : ¬ (δ (i delta))
+         := assume H : δ (i delta),
+            have H' : r (i delta) (i delta),
+              from eq_rec H (symm retract),
+            H H'.
diff --git a/tests/lean/run/cody2.lean b/tests/lean/run/cody2.lean
new file mode 100644
index 000000000..ac356b33d
--- /dev/null
+++ b/tests/lean/run/cody2.lean
@@ -0,0 +1,23 @@
+import logic
+
+abbreviation subsets (P : Type) := P → Prop.
+
+section
+
+hypothesis A : Type.
+
+hypothesis r : A → subsets A.
+
+hypothesis i : subsets A → A.
+
+hypothesis retract {P : subsets A} {a : A} : r (i P) a = P a.
+
+definition delta (a:A) : Prop := ¬ (r a a).
+
+notation `δ` := delta.
+
+theorem delta_aux : ¬ (δ (i delta))
+         := assume H : δ (i delta),
+            H (subst (symm retract) H).
+
+check delta_aux.
\ No newline at end of file