Re: [isabelle] I need a fixed mutable array
On Di, 2014-06-17 at 10:56 -0500, Gottfried Barrow wrote:
> I did a few searches to find whether there are mutable arrays in
> Isabelle. It appears there's not, though I found a little info:
HOL itself does not support mutable arrays.
However, there is Imperative_HOL, which has a heap monad supporting
Then there is afp/Collections/Lib/Diff_Array, which provides an
implementation of arrays that behaves purely functional, but is
efficient if only the last version is accessed.
However, if you are not after *efficient* executability, but only
looking for an abstract model of a memory, it makes no sense using the
above types, as the efficiency comes at teh price of additional
This archive was generated by a fusion of
Pipermail (Mailman edition) and