From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 7 Jun 2005 17:37:53 +0000 (+0000)
Subject: added test for coercions
X-Git-Tag: PRE_INDEX_1~47
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7c4e75d43137f6bc529d1c42a298a72a3548a912;p=helm.git

added test for coercions
---

diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma
new file mode 100644
index 000000000..21bf994ce
--- /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.
+
+
+
+
+
+
+
+
+
+