
  0 | ||| We can make any collection into an dependently indexed collection
  1 | ||| by storing dependent pairs.
  2 | module Data.Indexed.AddDep
  3 | 
  4 | import Data.Witherable
  5 | import Data.Witherable.Dependent
  6 | 
  7 | 
  8 | public export
  9 | record DepIndexed (t : Type -> Type) (i : Type) (a : i -> Type) where
 10 |   constructor AddDepIndex
 11 |   unDepIndex : t (DPair i a)
 12 | 
 13 | 
 14 | export
 15 | (Functor t) => DepFunctor i (DepIndexed t i) where
 16 |   dmap f (AddDepIndex p) = AddDepIndex (dmap f <$> p)
 17 | 
 18 | export
 19 | (Foldable t) => DepFoldable i (DepIndexed t i) where
 20 |   dfoldl f z (AddDepIndex p) = foldl (\u, (MkDPair x y) => f u x y) z p
 21 |   dfoldr f z (AddDepIndex p) = foldr (\(MkDPair x y), u => f x y u) z p
 22 | 
 23 | export
 24 | (Traversable t) => DepTraversable i (DepIndexed t i) where
 25 |   dtraverse f (AddDepIndex p) = AddDepIndex <$> traverse (dtraverse f) p
 26 | 
 27 | export
 28 | (Filterable t) => DepFilterable i (DepIndexed t i) where
 29 |   dmapMaybe f (AddDepIndex p) = AddDepIndex $ mapMaybe (dtraverse f) p
 30 | 
 31 | export
 32 | [depIndexedWitherable] (Witherable t) => DepWitherable i (DepIndexed t i) where
 33 | 
 34 |