added regtest for optional inductive type on mutcase

diff --git a/helm/gTopLevel/tests/match07.cic b/helm/gTopLevel/tests/match07.cic
new file mode 100644 (file)
index 0000000..15ead07
--- /dev/null
+++ b/helm/gTopLevel/tests/match07.cic
@@ -0,0 +1,4 @@
+[\lambda x:bool. nat]
+match true with
+[ true \Rightarrow O
+| false \Rightarrow (S O) ]

diff --git a/helm/gTopLevel/tests/match07.cic.test b/helm/gTopLevel/tests/match07.cic.test
new file mode 100644 (file)
index 0000000..ec1ad71
--- /dev/null
+++ b/helm/gTopLevel/tests/match07.cic.test
@@ -0,0 +1,16 @@
+[\lambda x:bool. nat]
+match true 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