[Why3-club] syntactic sugar
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.
More information about the Why3-club