
  0 | module Data.Container.Additive.Properties.Definition
  1 | 
  2 | import Data.ComMonoid
  3 | import Data.Container.Base.Definitions
  4 | import Data.Container.Base.Properties.Definition
  5 | import Data.Container.Additive.Object.Definition
  6 | 
  7 | ||| Convenience datatype storing the property that
  8 | ||| an additive container `c` has an interface `i` on its positions
  9 | public export
 10 | InterfaceOnPositions : (c : AddCont) -> (i : Type -> Type) -> Type
 11 | InterfaceOnPositions c = InterfaceOnPositions (UC c)
 12 | 
 13 | namespace Const
 14 |   public export
 15 |   data IsConst : AddCont -> Type where
 16 |     MkIsConst : (p : Type) -> (mon : ComMonoid p) =>
 17 |       IsConst (MkAddCont p (\_ => (p ** mon)))
 18 |