From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 3 Feb 2004 14:04:05 +0000 (+0000)
Subject: New tests for lambdas (that show bugs in applications ;-)
X-Git-Tag: V_0_2_3~97
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a3d7a85e807ab78dd7524c22b853fa5fbb2e2439;p=helm.git

New tests for lambdas (that show bugs in applications ;-)
---

diff --git a/helm/gTopLevel/tests/lambda01.cic b/helm/gTopLevel/tests/lambda01.cic
new file mode 100644
index 000000000..0c06ca4f6
--- /dev/null
+++ b/helm/gTopLevel/tests/lambda01.cic
@@ -0,0 +1,2 @@
+(\lambda f. (f 0 (le_n 0))
+  \lambda n. \lambda H. (refl_equal nat 0)))
diff --git a/helm/gTopLevel/tests/lambda02.cic b/helm/gTopLevel/tests/lambda02.cic
new file mode 100644
index 000000000..dc6d57916
--- /dev/null
+++ b/helm/gTopLevel/tests/lambda02.cic
@@ -0,0 +1 @@
+\lambda f:(\forall n:nat. (\forall H:(le 0 n). (n=n))). (f 0 (le_n 0))