[Why3-club] syntactic sugar

Alan Schmitt alan.schmitt at polytechnique.org
Fri Sep 21 17:26:45 CEST 2012


I see in array.mlw that it is possible to declare some syntactic sugar
to have a[i] be M.get a.elts i.

How would I change this to have a[i,j] or a[i][j] (whichever is
possible) as syntactic sugar for M.get a.elts (i,j)?



More information about the Why3-club mailing list