added test for coercions

diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma
new file mode 100644 (file)
index 0000000..21bf994
--- /dev/null
+++ b/helm/matita/tests/coercions.ma
@@ -0,0 +1,44 @@
+inductive pos: Set \def
+| one : pos
+| next : pos \to pos.
+
+inductive nat:Set \def
+| O : nat
+| S : nat \to nat.
+
+inductive int: Set \def
+| positive: nat \to int
+| negative : nat \to int.
+
+inductive empty : Set \def .
+
+let rec pos2nat (x:pos) : nat  \def 
+  match x with  
+  [ one \Rightarrow (S O)
+  | (next z) \Rightarrow S (pos2nat z)].
+
+let rec nat2int (x:nat) :int \def
+  match x with
+  [ O \Rightarrow positive O
+  | (S z) \Rightarrow positive (S z)].
+
+coercion pos2nat.
+
+coercion nat2int.
+
+let rec plus (x,y:int) on x : int \def
+  match x with
+  [ (positive n) \Rightarrow x
+  | (negative z) \Rightarrow y].
+
+theorem a: plus O one.
+
+
+
+
+
+
+
+
+
+