
  0 | ||| A DepFilterable is a dependently-typed Functor where elements can
  1 | ||| be thrown away.
  2 | module Data.Filterable.Dependent
  3 | 
  4 | import public Data.Functor.Dependent
  5 | 
  6 | 
  7 | public export
  8 | interface (DepFunctor i t) => DepFilterable (0 i : Type) (0 t : (i -> Type) -> Type) | t where
  9 |   dmapMaybe : {0 u : i -> Type} -> {0 v : i -> Type} -> ((x : i) -> u x -> Maybe (v x)) -> t u -> t v
 10 |   dmapMaybe f = dcatMaybes . dmap f
 11 | 
 12 |   dcatMaybes : {0 v : i -> Type} -> t (Maybe . v) -> t v
 13 |   dcatMaybes = dmapMaybe (\_, y => y)
 14 | 
 15 |   flush : {0 u : i -> Type} -> {0 v : i -> Type} -> t u -> t v
 16 |   flush = dmapMaybe (\_, _ => Nothing)
 17 |