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

David MENTRE dmentre at linux-france.org
Wed Nov 28 16:01:21 CET 2012


Hello Johannes,

2012/11/28 Johannes Kanig <kanig at adacore.com>:
>> """
>> module Test2
>>   use import ref.Ref
>>   use import array.Array
>>
>>   type t = array int
>>   val c : ref t
>
> In Why3, you are not allowed to store mutable objects in other mutable
> objects. Here, you are storing a mutable array in a reference.

Thanks! In my specific case I don't really need a mutable array so
I'll fall back to a map.

Best regards,
david



More information about the Why3-club mailing list