Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Issues regarding use of finite map interface (FMapInterface)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Issues regarding use of finite map interface (FMapInterface)


chronological Thread 
  • From: "St�phane Lescuyer" <lescuyer AT lri.fr>
  • To: "Brian Aydemir" <baydemir AT cis.upenn.edu>
  • Cc: "Sunil Kothari" <skothari AT uwyo.edu>, coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Issues regarding use of finite map interface (FMapInterface)
  • Date: Mon, 15 Sep 2008 10:25:47 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references:x-google-sender-auth; b=ZZyc1NROV5/Utkcvz+/RMRG9xC+wilnOQIeRureIeEDCmj9zTK0+mmFSpD7IxgTN4m fbNUjZ8UsIW72Ga6PmIfG+gjkN0VDflw8Q+UzCtxsROQ2uXPj7r9nYe5OfVYB20emBEE b0hTkhhUhtdzSkIJldanVVEiv9mwvwEzqhlaU=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Sun, Sep 14, 2008 at 8:14 PM, Brian Aydemir 
<baydemir AT cis.upenn.edu>
 wrote:
> Idiom #2: Use the signature to hide the details of the implementation.
>
> <<
> Module SomeFMapImpl : FMapInterface.S with E := Foo :=
>  FMapList.Make Foo.
>>>
>
> The ": FMapInterface.S with E := Foo" is key.  Without it, you'll be able to
> see the gory details of the implementation.  With it, you'll know only what
> FMapInterface.S reveals.

Just a remark on that: it's fine to hide the details and do that if
you re only interested in proofs, but restricting the output interface
of FMapList.Make to FMapInterface.S using the : operator (instead of
<:) will make the definitions of FMapList opaque, and as a result will
not allow you to actually compute operations over maps. So depending
on what you want to use FMaps for, you may or may not be able to use
that trick.

Stéphane
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06



Archive powered by MhonArc 2.6.16.

Top of Page