The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

I think [Axiom] and [Parameter] are synonyms in all contexts.

Marco, I will extend Cedric's advice by suggesting that you read the 
documentation not just on sections, but also on the module system.

AUGER Cedric wrote:
> Le Fri, 5 Aug 2011 12:30:51 +0200,
> Marco 
> Servetto<marco.servetto AT gmail.com>
>   a écrit :
>
>    
> > This library looks promising.
> > There is any documentation/guide/simple example of use of it?
> > (i'm not interested in exporting programs, i need it only to make
> > proofs)
> >
> > what is the meaning of
> >    Axiom eq_refl : forall m : t, eq m m.
> >    Axiom eq_sym : forall m1 m2 : t, eq m1 m2 ->  eq m2 m1.
> >   ....
> > It looks like it assert that some function have some properties
> > instead of requiring the user to provide such proofs.
> > It is right?
> >
> > And... err, my coq ignorance... what is the meaning of
> > "Parameter" it looks like it autodeclare a parameter with such
> > name/type in all the following function, but:
> >    -what is the scope of such declaration?
> >    -what is the difference with "Hypothesis"?
> >      
> See the chapter about "Sections" for more informations.
>
> Basically, the scope is between the declaration and the "End" of the
> deepest section at declaration time.
>
> A little like "Lemma" "Corollary" "Theorem" and
> "Definition",
> Parameter(s) is basically the same as Hypothesis (and
> Variable(s));
> I don't know if Axiom works the same way, I should take a look at the
> reference manual for more enlightment.
>