@[class]
- bind : Π {α β : Type ?}, m α → (α → m β) → m β
Instances
@[class]
- to_applicative : applicative m
- to_has_bind : has_bind m
Instances
- option.monad
- exceptional.monad
- interaction_monad.monad
- task.monad
- tactic.unsafe.type_context.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
- 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
- part.monad
Equations
- has_bind.seq x y = x >>= λ (_x : α), y