coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adam AT chlipala.net>
- To: Marco Servetto <marco.servetto AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Finite Maps
- Date: Sat, 06 Aug 2011 10:03:32 -0400
Marco Servetto wrote:
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." For instance, Coq module Coq.FSets.FSetAVL contains a functor for producing finite set implementations. This should be a complete answer to the question of "how to instantiate a map or set"; I hope further questions can be more specific.
Moreover, since setoid is required, Does setoid use extra axioms or not?
What makes you think "setoid is required"?
Is there a standard way to know if a library I'm using does use extra
axioms?
See the vernacular command [Print Assumptions].
- Re: [Coq-Club] Finite Maps, (continued)
- 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, Adam Chlipala
- 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.