From 16b982158e86f41a8eb6c2375da4d9b96e697b3d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 21 Jul 2009 20:25:12 +0000 Subject: [PATCH] 1) record projections are now automatically generated 2) incomplete code commented out --- helm/software/matita/nlibrary/algebra/magmas.ma | 2 ++ helm/software/matita/nlibrary/sets/sets.ma | 2 -- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index d74913988..df39c1b30 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -66,9 +66,11 @@ nqed. ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝ λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}. +(* ndefinition mm_counter_image: ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma A. #A; #B; #Ma; #Mb; #f; napply (mk_magma ???) [ napply (counter_image ?? f Mb) | #x; #y; nwhd in ⊢ (% → % → ?); *; #y0; *; #Hy0; #H +*) \ No newline at end of file diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index a12f1fc5c..07c7884ce 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -15,8 +15,6 @@ include "logic/equality.ma". nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }. -(* This is a projection! *) -ndefinition mem ≝ λA.λr:powerset A.match r with [mk_powerset f ⇒ f]. interpretation "powerset" 'powerset A = (powerset A). -- 2.39.2