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

Johannes Kanig kanig at adacore.com
Wed Nov 28 16:36:05 CET 2012

On 11/28/2012 04:31 PM, David MENTRE wrote:
> One solution would be to copy/paste array.mlw into staticarray.mlw and
> adapt it to my needs. I need to think about it (because I hate not
> reusing existing std library).

I don't understand what would be the difference between array.mlw and
staticarray.mlw? Do your "static" arrays have a static length? Static as
in "known at compile time", not as in "cannot be changed for a given array".

Johannes Kanig <kanig at adacore.com>

More information about the Why3-club mailing list