Data.Container.Additive.Object.Instances

Definitions

Scalar : AddCont

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

Visibility: public export

Empty : AddCont

  Empty additive container
  Unit of the coproduct
  Initial container

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

Visibility: public export

TrivialPos : Type -> AddCont

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

Visibility: public export