Idris2Doc : Data.Container.Additive.Extension.Definition

Data.Container.Additive.Extension.Definition

(source)
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
extMap : c =%+> d -> Ext c y -> Ext d y
  Analogous to one in `Base.Extension.Definition`

  Totality: total
  Visibility: public export