Test des coercions dans les motifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2284 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 36 insertions, 0 deletions

diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
new file mode 100644
index 000000000..06149b3fa
--- /dev/null
+++ b/test-suite/success/Case13.v
@@ -0,0 +1,36 @@
+(* Check coercions in patterns *)
+
+Inductive I : Set :=
+  C1 : nat -> I
+| C2 : I -> I.
+
+Coercion C1 : nat >-> I.
+
+(* Coercion at the root of pattern *)
+Check [x]Cases x of (C2 n) => O | O => O | (S n) => n end.
+
+(* Coercion not at the root of pattern *)
+Check [x]Cases x of (C2 O) => O | _ => O end.
+
+(* TODO: insert unification inside patterns to get these examples working
+
+Check [x:(option nat)]Cases x of None => O | (Some O) => O | _ => O end.
+
+(* Coercion up to delta-conversion *)
+Coercion somenat := (Some nat).
+Check [x]Cases x of None => O | O => O | (S n) => n end.
+
+*)
+
+(* Coercions with parameters *)
+Inductive listn : nat-> Set := 
+  niln : (listn O) 
+| consn : (n:nat)nat->(listn n) -> (listn (S n)).
+
+Inductive I' : nat -> Set :=
+  C1' : (n:nat) (listn n) -> (I' n)
+| C2' : (n:nat) (I' n) -> (I' n).
+
+Coercion C1' : listn >-> I'.
+Check [x:(I' O)]Cases x of (C2' _ _) => O | niln => O | _ => O end.
+Check [x:(I' O)]Cases x of (C2' _ niln) => O | _ => O end.