Re: [isabelle] What Isabelle maps to use to generate usual (ordered) maps



Hi Thomas,

in our developments we are using Isabelle's red-black trees for that purpose (HOL/Library/RBT.thy). We do also generate code (Haskell, SML, and Scala) and it works.

cheers

chris

On 07/01/2011 04:47 PM, Thomas Genet wrote:

Dear Isabelle users,

I am wondering what is the map theory that I have to use in order to
generate
usual ML maps: roughly trees ordered w.r.t. to keys?

By the way, I want to generate Scala code.


Thanks in advance,

Thomas






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.