coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marco Servetto <marco.servetto AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Finite Maps
- Date: Fri, 5 Aug 2011 12:30:51 +0200
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"?
- [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps,
Xavier Leroy
- Re: [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps,
AUGER Cedric
- Re: [Coq-Club] Finite Maps,
Adam Chlipala
- Re: [Coq-Club] Finite Maps,
AUGER Cedric
- Re: [Coq-Club] Finite Maps,
Marco Servetto
- Re: [Coq-Club] Finite Maps, Adam Chlipala
- Re: [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps, Adam Chlipala
- Re: [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps, Adam Chlipala
- Re: [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps,
Marco Servetto
- Re: [Coq-Club] Finite Maps,
AUGER Cedric
- Re: [Coq-Club] Finite Maps,
Adam Chlipala
- Re: [Coq-Club] Finite Maps,
AUGER Cedric
- Re: [Coq-Club] Finite Maps, Marco Servetto
- Re: [Coq-Club] Finite Maps,
Xavier Leroy
Archive powered by MhonArc 2.6.16.