From 400a9c45c1ef1c84416b992f4eea66ed784879d8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jan 2020 03:50:49 -0800
Subject: [PATCH] test: `CoeSort` test

---
 tests/lean/run/coeSort1.lean | 15 +++++++++++++++
 tests/lean/run/coeSort2.lean | 13 +++++++++++++
 2 files changed, 28 insertions(+)
 create mode 100644 tests/lean/run/coeSort1.lean
 create mode 100644 tests/lean/run/coeSort2.lean

diff --git a/tests/lean/run/coeSort1.lean b/tests/lean/run/coeSort1.lean
new file mode 100644
index 0000000000..7401786c57
--- /dev/null
+++ b/tests/lean/run/coeSort1.lean
@@ -0,0 +1,15 @@
+new_frontend
+
+universes u
+
+def Below (n : Nat) : Nat → Prop :=
+(· < n)
+
+def f {n : Nat} (v : Subtype (Below n)) : Nat :=
+v.val + 1
+
+instance pred2subtype {α : Type u} (p : α → Prop) : CoeSort (α → Prop) p (Type u) :=
+CoeSort.mk _ (Subtype p)
+
+def g {n : Nat} (v : Below n) : Nat :=
+v.val + 1
diff --git a/tests/lean/run/coeSort2.lean b/tests/lean/run/coeSort2.lean
new file mode 100644
index 0000000000..dcebc3f07d
--- /dev/null
+++ b/tests/lean/run/coeSort2.lean
@@ -0,0 +1,13 @@
+universe u
+
+structure Group :=
+(carrier : Type u) (mul : carrier → carrier → carrier) (one : carrier)
+
+instance GroupToType (g : Group) : CoeSort Group g (Type u) :=
+CoeSort.mk _ g.carrier
+
+new_frontend
+
+variable (g : Group.{1})
+
+#check fun (a b : g) => g.mul a b