library Examples/Groups

spec Group =
  sort s
  ops 0:s;
      -__ :s->s;
      __+__ :s*s->s, assoc
  forall x,y:s
  . x+(-x) = 0
  . x+0=x %(leftunit)%
  . 0+x=x %(rightunit)% %implied
end