mathlib3 documentation

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

Instances of this typeclass

• monad.to_has_bind
• filter.has_bind
• ultrafilter.has_bind
• computation.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
• free_group.monad
• free_add_group.monad
• free_abelian_group.monad
• mv_polynomial.monad
• lazy_list.monad
• plift.monad
• ulift.monad
• writer_t.monad
• cont_t.monad
• slim_check.gen.monad
• tactic.norm_fin.eval_fin_m.monad
• parser.monad
• pmf.monad
• pfun.monad
• computation.monad
• stream.seq1.monad
• free_magma.monad
• free_add_magma.monad
• free_semigroup.monad
• free_add_semigroup.monad
• semiquot.monad
• erased.monad
• stream.wseq.monad
• multiset.monad
• finset.monad

Instances of other typeclasses for monad

• monad.has_sizeof_inst