From eeb60c972db9d58e6559a0e501d4221ce808b50a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 24 Jul 2007 08:58:16 +0000 Subject: [PATCH] added test about dependent coercions --- .../matita/tests/coercions_dependent.ma | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 helm/software/matita/tests/coercions_dependent.ma diff --git a/helm/software/matita/tests/coercions_dependent.ma b/helm/software/matita/tests/coercions_dependent.ma new file mode 100644 index 000000000..b89abbf21 --- /dev/null +++ b/helm/software/matita/tests/coercions_dependent.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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/". + +include "nat/nat.ma". +include "list/list.ma". +include "decidable_kit/list_aux.ma". +(* tests from "Dependent Coersion" by Luo and Soloviev *) + +inductive vec (A : Type) : nat -> Type := + | vnil : vec A O + | vcons : ∀a:A.∀n:nat.vec A n -> vec A (S n). + +axiom c : ∀A,B.∀l:list A.vec B (length A l). + +axiom veclen : ∀A,n.vec A n -> nat. + +coercion cic:/matita/test/c.con. + +alias num (instance 0) = "natural number". +definition xxx := veclen nat ? [3; 4; 7]. -- 2.39.2