mathlib documentation

core / init.control.monad

@[class]
structure has_bind (m : Type uType v) :
Type (max (u+1) v)
  • bind : Π {α β : Type ?}, m α(α → m β)m β
Instances of this typeclass
Instances of other typeclasses for has_bind
  • has_bind.has_sizeof_inst
@[reducible]
def return {m : Type uType v} [monad m] {α : Type u} :
α → m α
Equations
def has_bind.seq {α β : Type u} {m : Type uType v} [has_bind m] (x : m α) (y : m β) :
m β
Equations