From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jan 2006 15:58:10 +0000 (+0000)
Subject: "Hiding" notation for implicit coercion. Cool.
X-Git-Tag: make_still_working~7810
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ff81867363f855a3ad5bba6f6bb636f20bf8a969;p=helm.git

"Hiding" notation for implicit coercion. Cool.
---

diff --git a/helm/matita/library/algebra/monoids.ma b/helm/matita/library/algebra/monoids.ma
index 9fd733042..c85d1ebc1 100644
--- a/helm/matita/library/algebra/monoids.ma
+++ b/helm/matita/library/algebra/monoids.ma
@@ -34,6 +34,12 @@ for @{ 'munit $S }.
 
 interpretation "Monoid unit" 'munit S =
  (cic:/matita/algebra/monoids/e.con S).
+ 
+notation < "M"
+for @{ 'semigroup $M }.
+
+interpretation "Semigroup coercion" 'semigroup M =
+ (cic:/matita/algebra/monoids/semigroup.con M).
 
 definition is_left_inverse ≝
  λM:Monoid.