interface IndexedMonad : (z : Type) -> (Type -> z -> z -> Type) -> Type- Parameters: z, m
Constraints: IndexedApplicative z m
Methods:
bind : m a i j -> (a -> m b j k) -> m b i k join : m (m a j k) i j -> m a i k
bind : IndexedMonad z m => m a i j -> (a -> m b j k) -> m b i k- Visibility: public export
join : IndexedMonad z m => m (m a j k) i j -> m a i k- Visibility: public export
(>>>=) : IndexedMonad z m => m a i j -> (a -> m b j k) -> m b i k- Visibility: public export
Fixity Declaration: infixl operator, level 1 (=<<<) : IndexedMonad z m => (a -> m b j k) -> m a i j -> m b i k Flipped version of `>>>=`
Visibility: public export
Fixity Declaration: infixl operator, level 1(>>>) : IndexedMonad z m => m () i j -> Lazy (m b j k) -> m b i k Sequence effects taking the value of the second.
Visibility: public export
Fixity Declaration: infixl operator, level 1(>>=>) : IndexedMonad z m => (a -> m b i j) -> (b -> m c j k) -> a -> m c i k Left-to-right Kleisli composition of indexed monads.
Visibility: public export
Fixity Declaration: infixl operator, level 1(<=<<) : IndexedMonad z m => (b -> m c j k) -> (a -> m b i j) -> a -> m c i k Right-to-left Kleisli composition of indexed monads, flipped version of `>=>`.
Visibility: public export
Fixity Declaration: infixl operator, level 1