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: 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].



Archive powered by MhonArc 2.6.16.

Top of Page