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 d749139882fb6da3209713a25af9ea9a2a850340..df39c1b3042a50683ae7a817c7b7d96656a02866 100644 (file)
--- 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 a12f1fc5c52dbc0a89b2ae6096b3e674080f79f9..07c7884ce7fc35cd153630ad059c181d3cee789d 100644 (file)
--- 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).