This commit was manufactured by cvs2svn to create branch 'moogle'.

[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
deleted file mode 100644 (file)
index 87bb015..0000000
--- a/helm/ocaml/cic_disambiguation/tests/match.txt
+++ /dev/null
@@ -1,49 +0,0 @@
-[\lambda x:nat.
-  [\lambda y:nat. Set]
-    match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]]
-match (S O):nat with
-[ O \Rightarrow O
-| (S x) \Rightarrow false ]
-
-[\lambda z:nat. \lambda h:(le O z). (eq nat O O)]
-match (le_n O): le with
-[ le_n \Rightarrow (refl_equal nat O)
-| (le_S x y) \Rightarrow (refl_equal nat O) ]
-
-[\lambda z:nat. \lambda h:(le (plus (plus O O) (plus O O)) z). (eq nat (plus (plus O O) (plus O O)) (plus (plus O O) (plus O O)))]
-match (le_n (plus (plus O O) (plus O O))): le with
-[ le_n \Rightarrow (refl_equal nat (plus (plus O O) (plus O O)))
-| (le_S x y) \Rightarrow (refl_equal nat (plus (plus O O) (plus O O))) ]
-
-(*
-[\lambda z:nat. \lambda h:(le 1 z). (le 0 z)]
-match (le_S 2 (le_n 1)): le with
-[ le_n \Rightarrow (le_S 1 (le_n 0))
-| (le_S x y) \Rightarrow y ]
-*)
-
-[\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))]
-match (le_S 0 0 (le_n 0)): le with
-[ le_n \Rightarrow (le_S 0 0 (le_n 0))
-| (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ]
-
-
-[\lambda x:bool. nat]
-match true:bool with
-[ true \Rightarrow O
-| false \Rightarrow (S O) ]
-
-[\lambda x:nat. nat]
-match O:nat with
-[ O \Rightarrow O
-| (S x) \Rightarrow (S (S x)) ]
-
-[\lambda x:list. list]
-match nil:list with
-[ nil \Rightarrow nil
-| (cons x y) \Rightarrow (cons x y) ]
-
-\lambda x:False.
-  [\lambda h:False. True]
-  match x:False with []
-