Data.ComMonoid

Definitions

record ComMonoid : Type -> Type

  Commutative monoid
  Not encoding the property of commutativity here

Totality: total
Visibility: public export
Constructor: 

MkComMonoid : (a -> a -> a) -> a -> ComMonoid a

Projections:

.neutral : ComMonoid a -> a

.plus : ComMonoid a -> a -> a -> a

Hints:

ComMonoid Double

ComMonoid ()

Num a => ComMonoid a

ComMonoid a => ComMonoid b => ComMonoid (a, b)

.plus : ComMonoid a -> a -> a -> a

Totality: total
Visibility: public export

plus : ComMonoid a -> a -> a -> a

Totality: total
Visibility: public export

.neutral : ComMonoid a -> a

Totality: total
Visibility: public export

neutral : ComMonoid a -> a

Totality: total
Visibility: public export

doubleIsMonoid : ComMonoid Double

Totality: total
Visibility: public export

unitIsMonoid : ComMonoid ()

Totality: total
Visibility: public export

numIsMonoid : Num a => ComMonoid a

Totality: total
Visibility: public export

listIsMonoid : ComMonoid (List a)

Totality: total
Visibility: public export

pairIsMonoid : ComMonoid a => ComMonoid b => ComMonoid (a, b)

Totality: total
Visibility: public export

sum : ComMonoid a => List a -> a

Totality: total
Visibility: public export

ComMonoid : Type

  Same as ComMonoid, but without exposing the underlying carrier in the type

Totality: total
Visibility: public export

ComMonoidHomo : ComMonoid -> ComMonoid -> Type

  Not encoding the rules for now

Totality: total
Visibility: public export