Idris2Doc : Data.Filterable.Indexed

Data.Filterable.Indexed

(source)

Reexports

import public Data.Filterable
import public Data.Functor.Indexed

Definitions

interface IndFilterable : Type -> (Type -> Type) -> Type
  An IndFilterable is a Filterable with read-only access to extra
indexing data.

Parameters: i, t
Constraints: Filterable t, IndFunctor i t
Methods:
imapMaybe : (i -> a -> Maybe b) -> t a -> t b

Implementations:
IndFilterable () Maybe
(Monad m, Alternative m) => IndFilterable a (Kleisli m a)
imapMaybe : IndFilterable i t => (i -> a -> Maybe b) -> t a -> t b
Visibility: public export
enumFilter : (Nat -> a -> Maybe b) -> List a -> List b
Visibility: export