The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

AUGER Cédric 
<Cedric.Auger AT lri.fr>
 writes:
>   Reserved Notation "a ** b" (at level 50).
> Section Monoid.
>   Variable Carrier: Set.
>   Variable mult_monoid: Carrier -> Carrier -> Carrier.
>   Notation "a ** b" := (mult_monoid a b).
>   Class Monoid :=
>   { neutral : Carrier

Yes, this is what I was previously doing; unfortunately [Section]s are
incompatible with [Module]s, which I would like to start using.


Bas Spitters 
<spitters AT cs.ru.nl>
 writes:
> Class SemiGroupOp A := sg_op: A → A → A.
> Infix "&" := sg_op (at level 50, left associativity).
> ...
>   Class Group {op: SemiGroupOp A} ...
>     ...
>     ; ginv_l: `(- x & x = mon_unit)

Ah, this is quite a nice trick!  It seems to work for my script.  Thank
you very much!


> Context A {e: Equiv A}.

By the way, how is the [Context] command different from [Variable]?  I
can't find [Context] in the manual:

  http://www.lix.polytechnique.fr/coq/refman/command-index.html

but my version of Coq certainly accepts it, and I see it appears once in
the Sozeau+Oury paper.  Is it just another synonym for [Variable]?

  - a