Data.Traversable.Dependent

A dependently-typed traversable class

Reexports

Definitions

interface DepTraversable : (i : Type) -> ((i -> Type) -> Type) -> Type

Parameters: i, t
Constraints: DepFoldable i t
Methods:

dtraverse : Applicative f => ((x : i) -> u x -> f (v x)) -> t u -> f (t v)

Implementations:

DepTraversable i (DPair i)

DepTraversable k (SortedDMap k)

dtraverse : DepTraversable i t => Applicative f => ((x : i) -> u x -> f (v x)) -> t u -> f (t v)

Visibility: public export