Idris2Doc : Data.Witherable.Dependent

Data.Witherable.Dependent

(source)
A dependently-typed Witherable

Reexports

import public Data.Filterable.Dependent
import public Data.Traversable.Dependent

Definitions

interface DepWitherable : (i : Type) -> ((i -> Type) -> Type) -> Type
Parameters: i, t
Constraints: DepTraversable i t, DepFilterable i t
Methods:
dwither : Applicative f => ((x : i) -> u x -> f (Maybe (v x))) -> t u -> f (t v)
dwither : DepWitherable i t => Applicative f => ((x : i) -> u x -> f (Maybe (v x))) -> t u -> f (t v)
Visibility: public export