# 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.