mathlib documentation

core.init.control.monad

@[class]
structure has_bind  :
(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] :
m α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] :
m αm βm β

Equations