The Coq mailing list

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

> What makes you think "setoid is required"?
-Library Coq.FSets.FMapInterface
requires
-Library Coq.Structures.DecidableType
that requires
-Library Coq.Lists.SetoidList
-that requires
Library Coq.Setoids.Setoid

>> Now, can I know what to do to instantiate my map and set?
> From the OCaml manual, you should have learned the concept of "functor."
Functor is a basic concept I was well aware before reading functor in
Ocaml, moreover it is well covered in section 2.5 you point me before.

>  For instance, Coq module Coq.FSets.FSetAVL contains a functor for producing
> finite set implementations.
Yes, as I have already written i have found some implementation
(including FSetAVL and Library Coq.FSets.FMapWeakInterface)
I was unable to understand what implementation does fit what interfaces.
----for maps:
WSfun, WS --> FMapWeakList,  and ???
WS
Sfun, S -->???
Sord -->???
---for sets:
WSfun --> may be ?FSetAVL and FSetList
WS-->???
Sfun-->???
S-->???
Sdep-->???

I would probably need both S[fun] and Sord for maps and S and Sdep from sets.



I have tried preddy hard, but from the page
http://coq.inria.fr/distrib/V8.2rc1/stdlib/Coq.FSets.FSetInterface.html
and
http://coq.inria.fr/distrib/V8.2rc1/stdlib/Coq.FSets.FMapInterface.html
there is no link to those hard finded files (well... actually
FMapWeakList is mentioned in the text, so with a little google you got
it, but.... I founded no way to have the complete list of all the
possible implementation presented in the standard library, with a
clear statement of what is implemented without having to lurk directly
into coq code...)

Marco.

p.s.
It tooks me a long time to realize that the module/functor
implementing the interface was the one called Raw.... It makes sense
with the idea of hiding the implementation, however it isn't making it
a little to extreem? may be someone want to depend of the
implementation...