From 47f4d2af2a592e2e6c0e0ea5f90ffae2fbf6391a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 10 Jul 2009 21:50:59 +0000 Subject: [PATCH] Composite coercions are here! --- helm/software/matita/nlibrary/algebra/magmas.ma | 4 ---- 1 file changed, 4 deletions(-) diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index e49d8ea82..f7757ba09 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -58,10 +58,6 @@ ndefinition mmmcarr ≝ ncoercion mmmcarr : ∀A,B,Ma,Mb.∀f: magma_morphism A B Ma Mb. pre_magma_morphism A B ≝ mmmcarr on _f: magma_morphism ???? to pre_magma_morphism ??. -ndefinition mmcarr_mmmcarr ≝ - λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb. mmcarr ?? (mmmcarr ???? f). -ncoercion mmcarr_mmmcarr : ∀A,B,Ma,Mb.∀f: magma_morphism A B Ma Mb. A → B ≝ mmcarr_mmmcarr - on _f: magma_morphism ???? to ∀_.?. ndefinition mmclosed ≝ λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb. match f return λf: magma_morphism A B Ma Mb.∀x. x ∈ Ma → f x ∈ Mb with -- 2.39.5