From: Enrico Tassi Date: Tue, 24 Jul 2007 08:58:16 +0000 (+0000) Subject: added test about dependent coercions X-Git-Tag: 0.4.95@7852~287 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20f2345a9a641c31a12ee77bf7fcd2e4e439b18e;p=helm.git added test about dependent coercions --- diff --git a/matita/tests/coercions_dependent.ma b/matita/tests/coercions_dependent.ma new file mode 100644 index 000000000..b89abbf21 --- /dev/null +++ b/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].