added coercions

[helm.git] / helm / matita / tests / match_inference.ma

diff --git a/helm/matita/tests/match_inference.ma b/helm/matita/tests/match_inference.ma
new file mode 100644 (file)
index 0000000..a84b3c3
--- /dev/null
+++ b/helm/matita/tests/match_inference.ma
@@ -0,0 +1,17 @@
+inductive pos: Set \def
+| one : pos
+| next : pos \to pos.
+
+inductive nat:Set \def
+| O : nat
+| S : nat \to nat.
+
+inductive empty : Set \def .
+
+definition pos2nat : pos \to nat  \def 
+     \lambda x:pos . match x with  
+      [ one \Rightarrow O 
+      | (next z) \Rightarrow O]. 
+
+definition empty2nat : empty \to nat  \def
+  \lambda x : empty . S (match x in empty with []).
\ No newline at end of file