
  0 | module Data.Container.Additive.Properties.Definition
  1 | 
  2 | import Data.Container.Base
  3 | import Data.Container.Additive.Object.Definition
  4 | 
  5 | ||| Convenience datatype storing the property that
  6 | ||| an additive container `c` has an interface `i` on its positions
  7 | public export
  8 | InterfaceOnPositions : (c : AddCont) -> (i : Type -> Type) -> Type
  9 | InterfaceOnPositions c = InterfaceOnPositions (UC c)