Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Finite Maps

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Finite Maps


chronological Thread 
  • 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"?



Archive powered by MhonArc 2.6.16.

Top of Page