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)

Num p => {auto mon : ComMonoid p} -> InterfaceOnPositions (Const p) Num

.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

  Every `Num` type is a commutative monoid under addition.
  Deliberately `export` and not `public export`, as it complicates search
  It spawns a witness for every `Const a` with numeric `a`

Totality: total
Visibility: 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

  Forgetful functor

Totality: total
Visibility: public export

ComMonoidHomo : ComMonoid -> ComMonoid -> Type

  Not encoding the rules for now
  Not using pattern matching so it reduces

Totality: total
Visibility: public export

functionIsMonoid : ComMonoid b -> ComMonoid (a -> b)

  Hom object of commutative monoids 
  Notably, without commutativity this does not exist

Totality: total
Visibility: public export

natMon : ComMonoid

  Natural numbers, the free commutative monoid on one generator.

Totality: total
Visibility: public export

Free : Type -> ComMonoid

Totality: total
Visibility: public export

fromGenerators : (a -> uSet y) -> ComMonoidHomo (Free a) y

  Hom-set isomorphism of the free-forgetful adjunction between ComMon and Set
  A map on generators is extended to a homomorphism out of a free commtuative 
  monoid on the 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`
  Special case of `fromGenerators` whe `a=Unit`.

Totality: total
Visibility: public export