mathlib3 documentation

• bind : Π {α β : Type ?}, m α → (α → m β) → m β

Instances of this typeclass

• monad.to_has_bind
• filter.has_bind
• ultrafilter.has_bind

Instances of other typeclasses for has_bind

• has_bind.has_sizeof_inst

• to_applicative : applicative m
• to_has_bind : has_bind m

Instances of this typeclass

• 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
• old_conv.monad
• trunc.monad
• with_one.monad
• with_zero.monad
• set.monad
• part.monad
• tactic.ring.ring_m.monad
• linarith.linarith_monad.monad
• tactic.ring_exp.ring_exp_m.monad
• ultrafilter.monad
• tactic.norm_fin.eval_fin_m.monad
• parser.monad

Instances of other typeclasses for monad

• monad.has_sizeof_inst