1. The last commit that fixed unification of compound coercions with

[helm.git] / helm / matita / library / algebra / semigroups.ma

diff --git a/helm/matita/library/algebra/semigroups.ma b/helm/matita/library/algebra/semigroups.ma
index d41c416f8484e9d0ce0c0e7143dd77a29b4d7608..5b461d1a4f43edba6acc9e4dd448f0eceb157243 100644 (file)
--- a/helm/matita/library/algebra/semigroups.ma
+++ b/helm/matita/library/algebra/semigroups.ma
@@ -16,38 +16,38 @@ set "baseuri" "cic:/matita/algebra/semigroups".
 
 include "higher_order_defs/functions.ma".
 
-definition isSemiGroup ≝
- λC:Type. λop: C → C → C.associative C op.
+(* Magmas *)
 
-record SemiGroup : Type ≝
- { carrier: Type;
-   op: carrier → carrier → carrier;
-   semigroup_properties: isSemiGroup carrier op
+record Magma : Type ≝
+ { carrier:> Type;
+   op: carrier → carrier → carrier
  }.
- 
-coercion cic:/matita/algebra/semigroups/carrier.con.
 
-notation "hvbox(a break \middot \sub S b)" 
-  left associative with precedence 55
-for @{ 'ptimes $S $a $b }.
+notation < "M" for @{ 'carrier $M }.
+interpretation "carrier coercion" 'carrier S =
+ (cic:/matita/algebra/semigroups/carrier.con S).
 
 notation "hvbox(a break \middot b)" 
   left associative with precedence 55
-for @{ 'ptimesi $a $b }.
+for @{ 'magma_op $a $b }.
 
-interpretation "Semigroup operation" 'ptimesi a b =
+interpretation "magma operation" 'magma_op a b =
  (cic:/matita/algebra/semigroups/op.con _ a b).
 
-(* too ugly
-interpretation "Semigroup operation" 'ptimes S a b =
- (cic:/matita/algebra/semigroups/op.con S a b). *)
-
-notation < "S"
-for @{ 'carrier $S }.
+(* Semigroups *)
 
-interpretation "Carrier coercion" 'carrier S =
- (cic:/matita/algebra/semigroups/carrier.con S).
+record isSemiGroup (M:Magma) : Prop ≝
+ { associative: associative ? (op M) }.
 
+record SemiGroup : Type ≝
+ { magma:> Magma;
+   semigroup_properties:> isSemiGroup magma
+ }.
+ 
+notation < "S" for @{ 'magma $S }.
+interpretation "magma coercion" 'magma S =
+ (cic:/matita/algebra/semigroups/magma.con S).
+ 
 definition is_left_unit ≝
  λS:SemiGroup. λe:S. ∀x:S. e·x = x.