interface IndexedApplicative : (z : Type) -> (Type -> z -> z -> Type) -> Type- Parameters: z, f
Constraints: IndexedFunctor z z f
Methods:
pure : a -> f a i iap : f (a -> b) i j -> f a j k -> f b i k
pure : IndexedApplicative z f => a -> f a i i- Visibility: public export
ap : IndexedApplicative z f => f (a -> b) i j -> f a j k -> f b i k- Visibility: public export
(<<*>>) : IndexedApplicative z f => f (a -> b) i j -> f a j k -> f b i k- Visibility: public export
Fixity Declaration: infixl operator, level 3 (<<*) : IndexedApplicative z f => f a i j -> f b j k -> f a i k- Visibility: public export
Fixity Declaration: infixl operator, level 3 (*>>) : IndexedApplicative z f => f a i j -> f b j k -> f b i k- Visibility: public export
Fixity Declaration: infixl operator, level 3 when : IndexedApplicative z f => Bool -> Lazy (f () i i) -> f () i i Conditionally execute an applicative expression when the boolean is true.
Visibility: public exportunless : IndexedApplicative z f => Bool -> Lazy (f () i i) -> f () i i Execute an applicative expression unless the boolean is true.
Visibility: public exporttraverse_ : (Foldable t, IndexedApplicative z f) => (a -> f b i i) -> t a -> f () i i Map each element of a structure to a computation, evaluate those
computations and discard the results.
Visibility: public exportsequence_ : (Foldable t, IndexedApplicative z f) => t (f a i i) -> f () i i Evaluate each computation in a structure and discard the results.
Visibility: public exportfor_ : (Foldable t, IndexedApplicative z f) => t a -> (a -> f b i i) -> f () i i Like `traverse_` but with the arguments flipped.
Visibility: public export