Data.Container.Additive.Properties.Definitions

Definitions

data InterfaceOnPositions : AddCont -> (Type -> Type) -> Type

  Convenience datatype storing the property that
  an additive container `c` has an interface `i` on its positions

Totality: total
Visibility: public export
Constructor: 

MkI : ((s : c .Shp) -> i (c .Pos s)) => InterfaceOnPositions c i

  For every shape s the set of positions c.Pos s has that interface

data IsFlat : AddCont -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsFlat : (p : Type) -> {auto mon : ComMonoid p} -> IsFlat (MkAddCont (Const p))