From 41818e7e1f465ca2062b1937dd432fc81fe777d6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 19 Jul 2006 15:11:14 +0000 Subject: [PATCH] Submitted a test for inferencing of dependent types. --- helm/software/matita/tests/apply2.ma | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 helm/software/matita/tests/apply2.ma diff --git a/helm/software/matita/tests/apply2.ma b/helm/software/matita/tests/apply2.ma new file mode 100644 index 000000000..220eddb4b --- /dev/null +++ b/helm/software/matita/tests/apply2.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/test/apply2". + +include "nat/nat.ma". + +(* in this test the type inferred for f is dependent! *) +definition test ≝ + ∀f,x. + f O (refl_eq nat O) = O ∧ + f x (refl_eq nat x) = O. + -- 2.39.2