Data.Filterable.Dependent

A DepFilterable is a dependently-typed Functor where elements can
be thrown away.

Reexports

Definitions

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

Parameters: i, t
Constraints: DepFunctor i t
Methods:

dmapMaybe : ((x : i) -> u x -> Maybe (v x)) -> t u -> t v

dcatMaybes : t (Maybe . v) -> t v

flush : t u -> t v

dmapMaybe : DepFilterable i t => ((x : i) -> u x -> Maybe (v x)) -> t u -> t v

Visibility: public export

dcatMaybes : DepFilterable i t => t (Maybe . v) -> t v

Visibility: public export

flush : DepFilterable i t => t u -> t v

Visibility: public export