The Coq mailing list

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

Quoting Daniel Schepler 
<dschepler AT gmail.com>:


> 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).
>
> ...

Hi Daniel and Matthieu,

Thank you for your answers.

I tried the solution with "Existing Instance", but
that directive didn't modify the behaviour of dot.

I wanted to avoid using decorations like (Monoid := ...)
because I had too many occurrences of dot to consider.

I tried succesfully an ugly solution :

Section foo.
  Notation dot := (dot (Monoid:= Z_add)).

Definition triple (z:Z) := dot z (dot z z).

End foo.

But I think that a local modification of the cost
would be very much better solution.






  The first


> End use_mult_monoid.
> --
> Daniel Schepler