From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 21 Jul 2009 20:25:12 +0000 (+0000)
Subject: 1) record projections are now automatically generated
X-Git-Tag: make_still_working~3640
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=16b982158e86f41a8eb6c2375da4d9b96e697b3d;p=helm.git

1) record projections are now automatically generated
2) incomplete code commented out
---

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).