E.1.2 Monoid

spec

Monoid =

sort

Elem

ops

n : Elem;
__*__ : Elem ×Elem -> Elem, assoc, unit n
%% Alternatively, just specify the corresponding axioms:

vars

x,y,z : Elem

·

n*x=x

·

x*n=x

·

(x*y)*z=x*(y*z)