The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Fri, 05 Aug 2011 08:04:34 -0400,
Adam Chlipala 
<adam AT chlipala.net>
 a écrit :

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

Oups, thanks Adam for this precision and response of my (implicit)
question on "Axiom" (although I will keep to use them the same way as
I used to, that is Axiom->declarations, I do not intend to implement/
Parameters->declarations, I intend to implement later since I do not
need a transparent implementation);

as I don't use Modules a lot, I completely forgot to tell that the
behaviour of Parameters is the same for both Section and Modules.

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