The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Yep, I have readed.
> Have you read Section 2.5 of the Coq manual, called "Module system"?  If
> that is not a sufficient introduction,

No, I dont
>have you read Chapter 2 of the OCaml
> manual, "The module system"?
>    http://caml.inria.fr/pub/docs/manual-ocaml/manual004.html
> OCaml's module system is the inspiration for Coq's.  Coq documentation is
> prone to avoid giving details on features that are inherited.
>
Wait... you are saing that in order to learn coq i must learn OCaml before??

The fact is that the
http://coq.inria.fr/stdlib/Coq.FSets.FMapInterface.html and
coresponding set
are, for what i can understand only the "interface" for maps,
I do understand that there are three different types of maps: WS S and Sord
what I can not find is: Where are the "implementation" modules (the
real modules and not the module types)
what implementation does corespond to WS S and Sord? I do belive to
have found some for WS, I'm in dubt for S but I found none for Sord.
More important, where is a guide with simple example where one can
understand how to start?
All this "documentation" i found is only autogenerated from coq
sources, there is no an english document that exaplain by simple
example how to use such maps/sets.

I can do
Definition myList : list nat:= [1;2;3] after importing the list.
What i have to do to obtain the same for finiteMap and set?