Data.ComMonoid

Reexports

Definitions

record ComMonoid : Type -> Type

  Commutative monoid
  Not encoding monoid laws, nor 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:

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

numIsMonoid : Num a => ComMonoid a

Totality: total
Visibility: public export

listIsMonoid : ComMonoid (List a)

Totality: total
Visibility: public export

bagIsMonoid : ComMonoid (Bag a)

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

sum : ComMonoid a => Bag 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

uSet : ComMonoid -> Type

Totality: total
Visibility: public export

ComMonoidHomo : ComMonoid -> ComMonoid -> Type

  Not encoding the rules for now

Totality: total
Visibility: public export

fromGenerators : {auto mon : ComMonoid y} -> (a -> y) -> ComMonoidHomo (Bag a ** bagIsMonoid) (y ** mon)

  One way of the hom-set isomorphism of the free-forgetful adjunction. It 
  extends a map on generators to a homomorphism out of the free commutative
  monoid on those generators.

Totality: total
Visibility: public export

scale : ComMonoid a => Nat -> a -> a

  Canonical action of `Nat` on a commutative monoid
  `scale n x` is the `n`-fold sum `x + ... + x`
  The one-generator case of `fromGenerators`, with `Nat \cong Bag Unit`

Totality: total
Visibility: public export