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.



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
usual ML maps: roughly trees ordered w.r.t. to keys?

By the way, I want to generate Scala code.

Thanks in advance,


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