-notation < "M" for @{ 'semigroup $M }.
-interpretation "premonoid coercion" 'premonoid M =
- (cic:/matita/algebra/monoids/premonoid.con M).
-
-notation < "M" for @{ 'typeofmonoid $M }.
-interpretation "premonoid coercion" 'typeofmonoid M =
- (cic:/matita/algebra/monoids/Type_of_Monoid.con M).
-
-notation < "M" for @{ 'magmaofmonoid $M }.
-interpretation "premonoid coercion" 'magmaofmonoid M =
- (cic:/matita/algebra/monoids/Magma_of_Monoid.con M).
-
-notation "1" with precedence 89
-for @{ 'munit }.
-
-interpretation "Monoid unit" 'munit =
- (cic:/matita/algebra/monoids/e.con _).