regression tests

[helm.git] / helm / gTopLevel / tests / match04.cic.test

diff --git a/helm/gTopLevel/tests/match04.cic.test b/helm/gTopLevel/tests/match04.cic.test
new file mode 100644 (file)
index 0000000..280bfbf
--- /dev/null
+++ b/helm/gTopLevel/tests/match04.cic.test
@@ -0,0 +1,16 @@
+[\lambda x:nat. nat]
+match O:nat with
+[ O \Rightarrow O
+| (S x) \Rightarrow (S (S x)) ]
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+
+<[x:nat]nat>Cases O of 
+ O => O
+ S => [x:nat](S (S x))
+end
+### (* TYPE_OF the disambiguated term *)
+([x:nat]nat O)
+### (* REDUCED disambiguated term     *)
+O