[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