@[class]
- bind : Π {α β : Type ?}, m α → (α → m β) → m β
@[class]
- to_applicative : applicative m
- to_has_bind : has_bind m
Instances
- option.monad
- exceptional.monad
- interaction_monad.monad
- task.monad
- id.monad
- except.monad
- except_t.monad
- state_t.monad
- reader_t.monad
- option_t.monad
- conv.monad
- vm_core.monad
- smt_tactic.monad
- tactic.unsafe.type_context.monad
- list.monad
- sum.monad
- monad_io_is_monad
- io_core_is_monad
- parser.monad
- old_conv.monad
- trunc.monad
- with_one.monad
- with_zero.monad
- set.monad
- tactic.ring.ring_m.monad
- linarith.linarith_monad.monad
- tactic.ring_exp.ring_exp_m.monad
- free_group.monad
- free_abelian_group.monad
- roption.monad
- pfun.monad
- computation.monad
- seq1.monad
- free_magma.monad
- free_add_magma.monad
- free_semigroup.monad
- free_add_semigroup.monad
- filter.ultrafilter.monad
- writer_t.monad
- cont_t.monad
- erased.monad
- semiquot.monad
- multiset.monad
- wseq.monad
- plift.monad
- ulift.monad
Equations
- has_bind.seq x y = x >>= λ (_x : α), y