Data.Container.Additive.Extension.Definition

Definitions

record Ext : (0 _ : AddCont) -> ComMonoid -> Type

  A functor `AddCont -> [ComMon, Type]`

Totality: total
Visibility: public export
Constructor: 

(<|) : (shapeExt : c .Shp) -> ComMonoidHomo (UMon c shapeExt) y -> Ext c y

Projections:

.index : ({rec:0} : Ext c y) -> ComMonoidHomo (UMon c (shapeExt {rec:0})) y

.shapeExt : Ext c y -> c .Shp

.shapeExt : Ext c y -> c .Shp

Totality: total
Visibility: public export

shapeExt : Ext c y -> c .Shp

Totality: total
Visibility: public export

.index : ({rec:0} : Ext c y) -> ComMonoidHomo (UMon c (shapeExt {rec:0})) y

Totality: total
Visibility: public export

index : ({rec:0} : Ext c y) -> ComMonoidHomo (UMon c (shapeExt {rec:0})) y

Totality: total
Visibility: public export