added tests

LPCIC · Nov 2, 2023 · 9f0c6cc · 9f0c6cc
1 parent c70c0e2
commit 9f0c6cc
Showing 1 changed file with 17 additions and 0 deletions.
diff --git a/apps/coercion/tests/test_coercion.v b/apps/coercion/tests/test_coercion.v
@@ -32,3 +32,20 @@ Check natmul R n : ringType_sort R.
 Check n : ringType_sort R.
 
 End TestNatMul.
+
+Elpi Accumulate coercion.db lp:{{
+
+coercion _ V T E {{ Nat.mul lp:V }} :-
+  coq.unify-eq T {{ nat }} ok,
+  coq.unify-eq E {{ nat -> nat }} ok.
+
+coercion _ V T E {{ { m : nat | m < lp:V } }} :-
+  coq.unify-eq T {{ nat }} ok,
+  coq.unify-eq E {{ Type }} ok.
+
+}}.
+Elpi Typecheck coercion.
+
+Check 3 2.
+Check forall (x : 3), proj1_sig x < 3.
+