Data.Container.Base.Object.Definition

Definitions

record Cont : Type

  Containers capture the idea that datatypes consist of groups of memory 
  locations where data can be stored. Locations for a particular group are 
  referred to as 'positions' and a particular group is referred to as a
  'shape'.

Totality: total
Visibility: public export
Constructor: 

(!>) : (Shp : Type) -> (Shp -> Type) -> Cont

Projections:

.Pos : ({rec:0} : Cont) -> Shp {rec:0} -> Type

  For each shape, a set of positions

.Shp : Cont -> Type

  A type of shapes

Hints:

ProdMonoid c => Alternative (Ext c)

TensorMonoid c => Applicative (Ext c)

IsNaperian c => Applicative (Ext c)

IsFoldable c => Foldable (Ext c)

Functor (Ext c)

Functor (Ext d . Ext c)

IsConcrete c => IsConcrete d => IsConcrete (c >< d)

IsConcrete c => IsConcrete d => IsConcrete (c >@ d)

SeqMonoid c => Monad (Ext c)

IsNaperian c => SeqMonoid c

SeqComonoid c -> TensorComonoid c

SeqMonoid c -> TensorMonoid c

IsNaperian c => TensorMonoid c

.Shp : Cont -> Type

  A type of shapes

Visibility: public export

Shp : Cont -> Type

  A type of shapes

Visibility: public export

.Pos : ({rec:0} : Cont) -> Shp {rec:0} -> Type

  For each shape, a set of positions

Visibility: public export

Pos : ({rec:0} : Cont) -> Shp {rec:0} -> Type

  For each shape, a set of positions

Visibility: public export