0 | module Algebra.Semigroup
 1 |
 2 | %default total
 3 |
 4 | ||| This interface is a witness that for a
 5 | ||| type `a` the axioms of a semigroup hold: `(<+>)` is associative.
 6 | |||
 7 | ||| Note: If the type is actually a monoid, use `Data.Algebra.LMonoid` instead.
 8 | public export
 9 | interface Semigroup a => LSemigroup a where
10 |   0 appendAssociative : {x,y,z : a} -> x <+> (y <+> z) === (x <+> y) <+> z
11 |
12 | ||| This interface is a witness that for a
13 | ||| type `a` the axioms of a commutative semigroup hold:
14 | ||| `(<+>)` is commutative.
15 | public export
16 | interface LSemigroup a => CommutativeSemigroup a where
17 |   0 appendCommutative : {x,y : a} -> x <+> y === y <+> x
18 |