Re: [isabelle] Imperative_HOL: code generator setup for Haskell

Hi Christian,

> 1) In Heap_Monad.thy there is a Haskell preamble including
> lengthArray :: STArray s a -> ST s Integer;
> lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
> Shouldn't that be the above +1? I thought in Haskell the bounds state
> the lowest and highest *index* of an array. So an array created with
> bound (0, k) should have length k+1. Maybe I'm wrong?

well, experimentally the second position of getBounds seems indeed to be
the *length*, not the highest index.  You may want to make two, three
examples to convince yourself.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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