[Why3-club] syntactic sugar

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Fri Sep 21 20:26:19 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)?

If you use a map of maps (instead of a map from pairs to values), then 
syntax a[i][j] can be used without any change.

-- 
Jean-Christophe



More information about the Why3-club mailing list