From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 13 Feb 2004 13:32:12 +0000 (+0000)
Subject: added regtest for optional inductive type on mutcase
X-Git-Tag: v0_0_4~202
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1d43744bf87522c418a8bb5d7787dcdbdd6f25a5;p=helm.git

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
index 000000000..15ead0774
--- /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
index 000000000..ec1ad7156
--- /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