regression tests

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

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