From a3d7a85e807ab78dd7524c22b853fa5fbb2e2439 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 3 Feb 2004 14:04:05 +0000 Subject: [PATCH] New tests for lambdas (that show bugs in applications ;-) --- helm/gTopLevel/tests/lambda01.cic | 2 ++ helm/gTopLevel/tests/lambda02.cic | 1 + 2 files changed, 3 insertions(+) create mode 100644 helm/gTopLevel/tests/lambda01.cic create mode 100644 helm/gTopLevel/tests/lambda02.cic 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)) -- 2.39.2