Algebra.Monoid

Definitions

interface LMonoid : Type -> Type

  This interface is a witness that for a
  type `a` the axioms of a monoid hold: `(<+>)` is associative
  with `neutral` being the neutral element.

Parameters: a
Constraints: Monoid a
Methods:

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

0 appendLeftNeutral : neutral <+> x = x

0 appendRightNeutral : x <+> neutral = x

Implementations:

LMonoid (List a)

LMonoid String

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

Totality: total
Visibility: public export

0 appendLeftNeutral : {auto __con : LMonoid a} -> neutral <+> x = x

Totality: total
Visibility: public export

0 appendRightNeutral : {auto __con : LMonoid a} -> x <+> neutral = x

Totality: total
Visibility: public export

interface CommutativeMonoid : Type -> Type

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

Parameters: a
Constraints: LMonoid a
Methods:

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

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

Totality: total
Visibility: public export