[Why3-club] Strange type error message on a ref array
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
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