From 1d43744bf87522c418a8bb5d7787dcdbdd6f25a5 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 13 Feb 2004 13:32:12 +0000
Subject: [PATCH] added regtest for optional inductive type on mutcase

---
 helm/gTopLevel/tests/match07.cic      |  4 ++++
 helm/gTopLevel/tests/match07.cic.test | 16 ++++++++++++++++
 2 files changed, 20 insertions(+)
 create mode 100644 helm/gTopLevel/tests/match07.cic
 create mode 100644 helm/gTopLevel/tests/match07.cic.test

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
-- 
2.39.2