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
def has_bind.and_then {α β : Type u} {m : Type uType v} [has_bind m] (x : m α) (y : m β) :
m β

Equations
  • x >> y = x >>= λ (_x : α), y
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