...

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
new file mode 100644 (file)
index 0000000..de8e3ba
--- /dev/null
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "sets/sets.ma".
+
+nrecord magma (A: Type) : Type ≝
+ { carr: Ω \sup A(*;
+   op: A → A → A;
+   op_closed: ∀x,y. x ∈ carr → y ∈ carr → op x y ∈ carr*)
+ }.
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index 857215f68a9477579c5faf0fc2eb13403ae71f61..1b7a60cdbc629aedf59437bd3b16392b8f5465ad 100644 (file)
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -1,3 +1,5 @@
-sets/sets.ma logic/connectives.ma
+sets/sets.ma logic/equality.ma
+logic/equality.ma logic/connectives.ma
 logic/connectives.ma logic/pts.ma
+algebra/magmas.ma sets/sets.ma
 logic/pts.ma 

diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot
index 7104158259e6c5106fbf1b64f6124a05bcf37794..eb6855410ab5062636773db9408f5e76023fac7e 100644 (file)
--- a/helm/software/matita/nlibrary/depends.dot
+++ b/helm/software/matita/nlibrary/depends.dot
@@ -1,8 +1,12 @@
 digraph g {
   "sets/sets.ma" [];
-  "sets/sets.ma" -> "logic/connectives.ma" [];
+  "sets/sets.ma" -> "logic/equality.ma" [];
+  "logic/equality.ma" [];
+  "logic/equality.ma" -> "logic/connectives.ma" [];
   "logic/connectives.ma" [];
   "logic/connectives.ma" -> "logic/pts.ma" [];
+  "algebra/magmas.ma" [];
+  "algebra/magmas.ma" -> "sets/sets.ma" [];
   "logic/pts.ma" [];
   
   }
\ No newline at end of file

diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png
index 631218af159fc61cadef10e8bce1304422377a7d..31bab15390047a8bf2cb44dd9a8720a13ea21c2a 100644 (file)
Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ

diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
new file mode 100644 (file)
index 0000000..d940b97
--- /dev/null
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/connectives.ma".
+
+ninductive eq (A: Type) (a: A) : A → Prop ≝
+ refl: eq A a a.
+ 
+interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+
+interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
\ 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 5ba0b08a6f856a40e3199c5cbda4fe439b53def0..a12f1fc5c52dbc0a89b2ae6096b3e674080f79f9 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "logic/connectives.ma".
+include "logic/equality.ma".
 
 nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }.
 (* This is a projection! *)
@@ -49,8 +49,6 @@ ndefinition union ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∨ x ∈ V }.
 
 interpretation "union" 'union U V = (union ? U V).
 
-(*
 ndefinition singleton ≝ λA.λa:A.{b | a=b}.
 
 interpretation "singleton" 'singl a = (singleton ? a).
-*)
\ No newline at end of file