Data.Container.Additive.Object.Instances

Definitions

Scalar : AddCont

  Scalar additive container
  This is equivalent to `!! UnitCont`
  Unit of the categorical product

Totality: total
Visibility: public export

Empty : AddCont

  Empty additive container
  Unit of the coproduct
  Initial container

Totality: total
Visibility: public export

Const : Type -> ComMonoid -> AddCont

  Constant additive container, positions not dependent on shapes
  Allows the backward part to be different than forward one

Totality: total
Visibility: public export

TrivialPos : Type -> AddCont

Totality: total
Visibility: public export

Dist : Nat -> AddCont

  Additive variant of the `Dist`  container. Shape is the type of 
  distributions over `n` choices, and position the *list* of choices made
  Note the similarities and differences with `Simplex`

Totality: total
Visibility: public export

Const : (a : Type) -> ComMonoid a => AddCont

  Like above, but where backward part is same as forward one
  Also arises from Num instance

Totality: total
Visibility: public export