Algebra.Semigroup

Definitions

interface LSemigroup : Type -> Type

  This interface is a witness that for a
  type `a` the axioms of a semigroup hold: `(<+>)` is associative.
  
  Note: If the type is actually a monoid, use `Data.Algebra.LMonoid` instead.

Parameters: a
Constraints: Semigroup a
Methods:

0 appendAssociative : x <+> (y <+> z) = (x <+> y) <+> z

Implementation: 

CommutativeSemigroup a -> LSemigroup a

0 appendAssociative : {auto __con : LSemigroup a} -> x <+> (y <+> z) = (x <+> y) <+> z

Totality: total
Visibility: public export

interface CommutativeSemigroup : Type -> Type

  This interface is a witness that for a
  type `a` the axioms of a commutative semigroup hold:
  `(<+>)` is commutative.

Parameters: a
Constraints: LSemigroup a
Methods:

0 appendCommutative : x <+> y = y <+> x

0 appendCommutative : {auto __con : CommutativeSemigroup a} -> x <+> y = y <+> x

Totality: total
Visibility: public export