mathlib documentation

core / init.control.monad

source
@[class]
structure has_bind (m : Type u → Type v) :
Type (max (u+1) v)
  • bind : Π {α β : Type ?}, m α → (α → m β) → m β
Instances
source
def has_bind.and_then {α β : Type u} {m : Type u → Type v} [has_bind m] (x : m α) (y : m β) :
m β
Equations
  • x >> y = x >>= λ (_x : α), y
source
@[class]
structure monad (m : Type u → Type v) :
Type (max (u+1) v)
Instances
source
def return {m : Type u → Type v} [monad m] {α : Type u} :
α → m α
Equations
source
def has_bind.seq {α β : Type u} {m : Type u → Type v} [has_bind m] (x : m α) (y : m β) :
m β
Equations