
  0 | module Data.Container.Additive.Properties.Definitions
  1 | 
  2 | import Data.Container.Base
  3 | import Data.Container.Additive.Object.Definition
  4 | 
  5 | import Data.ComMonoid
  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 | 
 14 | 
 15 | namespace Const
 16 |   public export
 17 |   data IsConst : AddCont -> Type where
 18 |     MkIsConst : (p : Type) -> (mon : ComMonoid p) => IsConst (MkAddCont (Const p))