
  0 | ||| A dependently-typed Witherable
  1 | module Data.Witherable.Dependent
  2 | 
  3 | import public Data.Filterable.Dependent
  4 | import public Data.Traversable.Dependent
  5 | 
  6 | 
  7 | public export
  8 | interface (DepTraversable i t, DepFilterable i t) => DepWitherable (0 i : Type) (0 t : (i -> Type) -> Type) | t where
  9 |   dwither : (Applicative f) => {0 u : i -> Type} -> {0 v : i -> Type} -> ((x : i) -> u x -> f (Maybe (v x))) -> t u -> f (t v)
 10 |   dwither f = map dcatMaybes . dtraverse f
 11 |