252N/Atype s, t

252N/A

252N/Aop a, b : s

252N/A

252N/A%% op __ + __ : s -> s -> s, idem, assoc, comm;

252N/A

252N/Aop __ + __ : t * t -> t

252N/Aop __ + __ : t -> t -> t

252N/Aop __ + __ : s * s -> s

252N/A

252N/A%%op a,b : t

252N/A

252N/A%%op c : s = a + b

252N/A

252N/Avar x:s

252N/A

252N/Aop y:s = (var x:s) + (var x:s)