0 | module Data.Container.Additive.Object.Instances
 1 |
 2 | import Data.List.Quantifiers
 3 | import Data.Vect.Quantifiers
 4 |
 5 | import Data.Container.Base
 6 | import Data.ComMonoid
 7 | import Data.Container.Additive.Object.Definition
 8 | import Data.Container.Additive.Extension.Definition
 9 |
10 | ||| Scalar additive container
11 | public export
12 | Scalar : AddCont
13 | Scalar = MkAddCont Scalar
14 |
15 | ||| Constant additive container, positions not dependent on shapes
16 | ||| Allows the backward part to be different than forward one
17 | public export
18 | Const : Type -> ComMonoid -> AddCont
19 | Const a (t ** m) = MkAddCont (Const2 a t) @{MkI @{\_ => m}}
20 |
21 | public export
22 | TrivialPos : Type -> AddCont
23 | TrivialPos a = Const a (Unit ** %search)
24 |
25 | namespace NumConst
26 |   ||| Like above, but where backward part is same as forward one
27 |   ||| Also arises from Num instance
28 |   public export
29 |   Const : (a : Type) -> (mon : ComMonoid a) => AddCont
30 |   Const a = Const a (a ** mon)