The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

Le Thu, 15 Apr 2010 03:45:17 +0000,
Adam Megacz 
<megacz AT cs.berkeley.edu>
 a écrit :

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

What do you mean with that? You can perfectly open a section inside a
module (I am almost certain that you also can open a module inside a
section, but that is not the problem here).

About modules, I expect you to have good reason to use them, as in Coq,
they are a lot less interesting as one can think at first glance.
Records, Type Classes, and Inductives, are almost as powerfull (and
are even often more powerfull) as Modules.

http://coq.inria.fr/cocorico/RecordsNotModules

That post was a little too excessive, I tried to moderate it with

http://coq.inria.fr/cocorico/ModulesNotRecords

what I wrote in the latter may be not correct nor complete, but I tried
to write down my little experience on it (I didn't write the previous).

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