From 06beff327fd71c8c6875860c76549d2ab142c6ec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Jul 2014 14:43:55 +0100
Subject: [PATCH] test(tests/lean/run): add more universe tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/run/coe5.lean | 40 ++++++++++++++++++++++++++++++++++++++++
 tests/lean/run/id.lean   | 12 ++++++++++++
 2 files changed, 52 insertions(+)
 create mode 100644 tests/lean/run/coe5.lean
 create mode 100644 tests/lean/run/id.lean

diff --git a/tests/lean/run/coe5.lean b/tests/lean/run/coe5.lean
new file mode 100644
index 000000000..8714ec5ae
--- /dev/null
+++ b/tests/lean/run/coe5.lean
@@ -0,0 +1,40 @@
+import standard
+
+namespace setoid
+  inductive setoid : Type :=
+  | mk_setoid: Π (A : Type'), (A → A → Bool) → setoid
+
+  set_option pp.universes true
+
+  check setoid
+  definition test : Type.{2} := setoid.{0}
+
+  definition carrier (s : setoid)
+  := setoid_rec (λ a eq, a) s
+
+  definition eqv {s : setoid} : carrier s → carrier s → Bool
+  := setoid_rec (λ a eqv, eqv) s
+
+  infix `≈`:50 := eqv
+
+  coercion carrier
+
+  inductive morphism (s1 s2 : setoid) : Type :=
+  | mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
+
+  check mk_morphism
+  check λ (s1 s2 : setoid), s1
+  check λ (s1 s2 : Type), s1
+
+  inductive morphism2 (s1 : setoid) (s2 : setoid) : Type :=
+  | mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2
+
+  check morphism2
+  check mk_morphism2
+
+  inductive my_struct : Type :=
+  | mk_foo : Π (s1 s2 : setoid) (s3 s4 : setoid), morphism2 s1 s2 → morphism2 s3 s4 → my_struct
+
+  check my_struct
+  definition tst2 : Type.{4} := my_struct.{1 2}
+end
\ No newline at end of file
diff --git a/tests/lean/run/id.lean b/tests/lean/run/id.lean
new file mode 100644
index 000000000..dc0fa0abc
--- /dev/null
+++ b/tests/lean/run/id.lean
@@ -0,0 +1,12 @@
+import standard
+definition id {A : Type} (a : A) := a
+check id id
+set_option pp.universes true
+check id id
+check id Bool
+check id num.num
+check @id.{0}
+check @id.{1}
+check id num.zero
+check @eq
+check eq eq