From 6ca120bf7773dd3a9ccb1e8b3ee2b4b8e7ff26af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Jul 2014 08:17:46 -0700
Subject: [PATCH] test(tests/lean/run): add Cody's file to test suite

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/run/univ1.lean | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 tests/lean/run/univ1.lean

diff --git a/tests/lean/run/univ1.lean b/tests/lean/run/univ1.lean
new file mode 100644
index 000000000..5ec2c524c
--- /dev/null
+++ b/tests/lean/run/univ1.lean
@@ -0,0 +1,29 @@
+import standard
+
+namespace S1
+hypothesis I : Type
+definition F (X : Type) : Type := (X → Prop) → Prop
+hypothesis unfold.{l} : I.{l} → F I.{l}
+hypothesis fold.{l}   : F I.{l} → I.{l}
+hypothesis iso1 : ∀x, fold (unfold x) = x
+end
+
+namespace S2
+universe u
+hypothesis I : Type.{u}
+definition F (X : Type) : Type := (X → Prop) → Prop
+hypothesis unfold : I → F I
+hypothesis fold   : F I → I
+hypothesis iso1 : ∀x, fold (unfold x) = x
+end
+
+
+namespace S3
+section
+  hypothesis I : Type
+  definition F (X : Type) : Type := (X → Prop) → Prop
+  hypothesis unfold : I → F I
+  hypothesis fold   : F I → I
+  hypothesis iso1 : ∀x, fold (unfold x) = x
+end
+end