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

Johannes Kanig kanig at adacore.com
Thu Nov 29 09:41:09 CET 2012


On 11/28/2012 06:37 PM, Andrei Paskevich wrote:
> On 28 November 2012 15:52, Johannes Kanig <kanig at adacore.com> wrote:
>> In Why3, you are not allowed to store mutable objects in other mutable
>> objects.
> Since Why3 v0.80, you are. 

Well that's really cool and thanks for correcting me. Sorry for the
noise, David!

Johannes

-- 
Johannes Kanig <kanig at adacore.com>



More information about the Why3-club mailing list