Data.Container.Additive.Properties.Definition

Definitions

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

data IsConst : AddCont -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsConst : (p : Type) -> {auto mon : ComMonoid p} -> IsConst (MkAddCont p (\{_:7199} => (p ** mon)))