From 448920d42f3f7886d27477281b22f0c11771d4ed Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 10 Jul 2009 16:10:54 +0000 Subject: [PATCH] more work on coercions composition --- helm/software/matita/tests/ng_coercions.ma | 68 ++++++++++++++-------- 1 file changed, 44 insertions(+), 24 deletions(-) diff --git a/helm/software/matita/tests/ng_coercions.ma b/helm/software/matita/tests/ng_coercions.ma index 308697d3c..3e22b3410 100644 --- a/helm/software/matita/tests/ng_coercions.ma +++ b/helm/software/matita/tests/ng_coercions.ma @@ -14,29 +14,49 @@ include "ng_pts.ma". -ninductive list (A : Type) : Type ≝ - | nil : list A - | cons : A → list A → list A. - +(* easy *) naxiom T : Type. naxiom S : Type. -naxiom c : list T → list S. - -ncoercion foo : ∀_l:list T. list S ≝ c - on _l : list T - to list ?. - -naxiom P : list S → Prop. - -ndefinition t1 ≝ ∀x:list T.P x → ?. ##[ napply Prop; ##] nqed. - -ncoercion bar : ∀_l:list T. S → S ≝ λ_.λx.x - on _l : list T - to Π_.?. - -naxiom Q : (S → S) → Prop. - -ndefinition t2 ≝ ∀x:list T.Q x → ?. ##[ napply Prop; ##] nqed. - - - \ No newline at end of file +naxiom R : Type. +naxiom U : Type. +naxiom c : T → S. +naxiom c1 : S → R. +naxiom c2 : R → U. + +ncoercion foo1 : ∀_t:T.S ≝ c on _t : T to S. +ncoercion foo2 : ∀_r:R.U ≝ c2 on _r : R to U. +ncoercion foo3 : ∀_s:S.R ≝ c1 on _s : S to R. + +(* another *) + +naxiom nat : Type. +naxiom A : nat → Type. +naxiom B : nat → Type. +naxiom C : nat → Type. +naxiom D : nat → Type. +naxiom a : ∀n:nat. A n → B n. +naxiom a1 : ∀n:nat. B n → C n. +naxiom a2 : ∀n:nat. C n → D n. + +ncoercion foo1 : ∀n:nat. ∀_a:A n. B n ≝ a on _a : A ? to B ?. +ncoercion foo2 : ∀n:nat. ∀_c:C n. D n ≝ a2 on _c : C ? to D ?. +ncoercion foo3 : ∀n:nat. ∀_b:B n. C n ≝ a1 on _b : B ? to C ?. + +naxiom cx : ∀n,m:nat. B n → C m. + +ncoercion foo3 : ∀n,m:nat. ∀_b:B n. C m ≝ cx on _b : B ? to C ?. + +naxiom Suc : nat → nat. +naxiom cs : ∀n:nat. B n → C (Suc n). + +ncoercion foo3 : ∀n:nat. ∀_b:B n. C (Suc n) ≝ cs on _b : B ? to C ?. + +(* funclass *) +naxiom Y : Type. +naxiom W : Type. +naxiom X : Type. +naxiom f : Y → W. +naxiom g : W → X → X → X. + +ncoercion foo : ∀_y:Y. W ≝ f on _y : Y to W. +ncoercion foo : ∀_w:W. X → X → X ≝ g on _w : W to Π_.Π_.?. -- 2.39.2