From 7c4e75d43137f6bc529d1c42a298a72a3548a912 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 7 Jun 2005 17:37:53 +0000
Subject: [PATCH] added test for coercions

---
 helm/matita/tests/coercions.ma | 44 ++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 helm/matita/tests/coercions.ma

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.
+
+
+
+
+
+
+
+
+
+
-- 
2.39.2