]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/tests/match.txt
snapshot, almost working
[helm.git] / helm / ocaml / cic_disambiguation / tests / match.txt
diff --git a/helm/ocaml/cic_disambiguation/tests/match.txt b/helm/ocaml/cic_disambiguation/tests/match.txt
new file mode 100644 (file)
index 0000000..0003a0c
--- /dev/null
@@ -0,0 +1,18 @@
+[nat]
+match true:bool with
+[ true \Rightarrow O
+| false \Rightarrow (S O)
+]
+
+[nat]
+match O:nat with
+[ O \Rightarrow O
+| (S x) \Rightarrow (S (S x))
+]
+
+[nat]
+match nil:list with
+[ nil \Rightarrow nil
+| (cons x y) \Rightarrow (cons x y)
+]
+