The Coq mailing list

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

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.