[isabelle] syntax



Hello,

I have a programming construct  construct of the following form:

update (% (x::'a, y::'b, z::'c): {(x'::', y'::'b, z::'c) . x' = x+1 /\ y'=y / 2 /\ z' = z + x + y})

Is it possible to introduce the syntax:

[: x::'a, y::'b, z::'c := x'::'a, y'::'b, z::'c . x' = x+1 /\ y'=y / 2 /\ z' = z + x + y :]

or

[: x, y, z := x', y', z . (x'::'a) = x+1 /\ (y'::'b)=y / 2 /\ (z'::'c) = z + x + y :]

Best regards,

Viorel





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.