The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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