The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Monday 11 April 2011 09:02:32 Matthieu Sozeau wrote:
> Le 11 avr. 2011 à 17:51, Pierre Casteran a écrit :
> > 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)  ?
> 
> Hi,
> 
> You can specify different costs for the instances, and the matching
> instances of the lowest cost are applied first. This can only be set
> globally, at definition time (at least for now). The syntax is [Instance
> foo: Bar A | 10] where 10 is the cost.
> -- Matthieu

For local overriding of the default: for a one-shot thing, I believe you 
could 
use "fun z:Z => dot z (dot z z (Monoid:=Z_mult)) (Monoid:=Z_mult)".

And in a section, you might be able to do (untested):

Section use_mult_monoid.

Existing Instance Z_mult.

Let cube (z:Z) := dot z (dot z z).

...

End use_mult_monoid.
-- 
Daniel Schepler