mathlib documentation

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

Instances

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

• 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
• mv_polynomial.monad
• free_group.monad
• free_abelian_group.monad
• computation.monad
• seq1.monad
• roption.monad
• pfun.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
• lazy_list.monad
• multiset.monad
• wseq.monad
• plift.monad
• ulift.monad
• slim_check.gen.monad