[Why3-club] syntactic sugar

Yannick Moy moy at adacore.com
Mon Sep 24 09:49:08 CEST 2012


On 09/24/2012 09:23 AM, Alan Schmitt wrote:

> Using this, I get the error (on the "a[i][j]" syntax):
>
> Bad arity: symbol ([]) must be applied to 3 arguments, but is applied to
> 2
>
> What am I doing wrong? And where can I find some documentation about
> this syntactic sugar?

I would expect something like a[i,j] instead of a[i][j], but the syntax 
of Why3 as documented in the manual only supports bracket notation with 
a single term inside the brackets. So it seems your use of brackets is 
not supported. (and the definition should be rejected in that case by Why3)
-- 
Yannick Moy, Senior Software Engineer, AdaCore



More information about the Why3-club mailing list