From 952974f024c823aa68166110097699ef077dd8ba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 21 Sep 2016 17:10:56 -0700
Subject: [PATCH] test(tests/lean/run/pred_to_subtype_coercion): add coercion
 to subtype test

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

diff --git a/tests/lean/run/pred_to_subtype_coercion.lean b/tests/lean/run/pred_to_subtype_coercion.lean
new file mode 100644
index 0000000000..9d4f80676b
--- /dev/null
+++ b/tests/lean/run/pred_to_subtype_coercion.lean
@@ -0,0 +1,18 @@
+universe variables u
+
+attribute [instance]
+definition pred2subtype {A : Type u} : has_coe_to_sort (A → Prop) :=
+⟨Type (max 1 u), λ p : A → Prop, subtype p⟩
+
+definition below (n : nat) : nat → Prop :=
+λ i, i < n
+
+check λ x : below 10, x
+
+definition f : below 10 → nat
+| ⟨a, h⟩ := a
+
+lemma zlt10 : 0 < 10 :=
+sorry
+
+check f ⟨0, zlt10⟩