The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello,

  I define a class

   Class Monoid (A:Type) : Type := {
  dot : A -> A -> A;
  id : A;
  dot_assoc : forall x y z:A, dot x (dot y z)= dot (dot x y) z;
  id_left : forall x, dot id x = x;
  id_right : forall x, dot x id = x}.

   and build two instances on Z of class (Monoid Z)  : Z_add (additive 
monoid) and
Z_mult (multiplicative monoid).

  Is there a simple way to specify (locally or globally)  which of both 
instances can
be considered as the default one, when analyzing an undecorated  term 
like for instance
fun z:Z => dot z (dot z z)  ?


Pierre