test: CoeSort test

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

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