From 47f4d2af2a592e2e6c0e0ea5f90ffae2fbf6391a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it> 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.2