[Why3-club] Strange type error message on a ref array

Johannes Kanig kanig at adacore.com
Wed Nov 28 16:13:48 CET 2012

On 11/28/2012 04:01 PM, David MENTRE wrote:
> Thanks! In my specific case I don't really need a mutable array so
> I'll fall back to a map.

Sounds good, but note that the type array is already basically a
reference to a map. The only difference is that the type array also
comes with the length of the array, and index validity preconditions for
the access/update.

So if you don't need the length stuff, then "ref + map" is good,
otherwise you can also use "array" directly.

Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list