
  0 | ||| We can regard any functor as dependently indexed, with specified
  1 | ||| fixed index.
  2 | module Data.Indexed.FixedDep
  3 | 
  4 | import Data.Witherable
  5 | import Data.Witherable.Dependent
  6 | 
  7 | 
  8 | public export
  9 | record FixDepIndex {0 i : Type} (x : i) (f : Type -> Type) (a : i -> Type) where
 10 |   constructor WithDepIndex
 11 |   unIndex : f (a x)
 12 | 
 13 | 
 14 | export
 15 | {x : i} -> Functor f => DepFunctor i (FixDepIndex x f) where
 16 |   dmap f (WithDepIndex m) = WithDepIndex $ map (f x) m
 17 | 
 18 | export
 19 | {x : i} -> Foldable f => DepFoldable i (FixDepIndex x f) where
 20 |   dfoldl f z (WithDepIndex m) = foldl (\i => f i x) z m
 21 |   dfoldr f z (WithDepIndex m) = foldr (f x) z m
 22 | 
 23 | export
 24 | {x : i} -> Traversable f => DepTraversable i (FixDepIndex x f) where
 25 |   dtraverse f (WithDepIndex m) = WithDepIndex <$> traverse (f x) m
 26 | 
 27 | export
 28 | {x : i} -> Filterable f => DepFilterable i (FixDepIndex x f) where
 29 |   dmapMaybe f (WithDepIndex m) = WithDepIndex $ mapMaybe (f x) m
 30 | 
 31 | export
 32 | {x : i} -> Witherable f => DepWitherable i (FixDepIndex x f) where
 33 |   dwither f (WithDepIndex m) = WithDepIndex <$> wither (f x) m
 34 |