Data.Withering.Dependent

A dependently-typed Withering

Definitions

data DepWithering : (Type -> Type) -> (i : Type) -> (i -> Type) -> (i -> Type) -> Type

Totality: total
Visibility: public export
Constructor: 

MkDepWithering : Applicative f => (DepWitherable i t => t u -> f (t v)) -> DepWithering f i u v

runDepWither : DepWitherable i t => DepWithering f i u v -> t u -> f (t v)

Visibility: export

depWitherOne : DepWithering f i u v -> (x : i) -> u x -> f (Maybe (v x))

Visibility: export

preserving : Applicative f => DepWithering f i u u

Visibility: export

flushing : Applicative f => DepWithering f i u v

Visibility: export

mapping : Applicative f => ((x : i) -> u x -> v x) -> DepWithering f i u v

Visibility: export

mapMaybeing : Applicative f => ((x : i) -> u x -> Maybe (v x)) -> DepWithering f i u v

Visibility: export

traversing : Applicative f => ((x : i) -> u x -> f (v x)) -> DepWithering f i u v

Visibility: export

withering : Applicative f => ((x : i) -> u x -> f (Maybe (v x))) -> DepWithering f i u v

Visibility: export

depWithering : Withering f i a b -> DepWithering f i (const a) (const b)

Visibility: export