mathlib3 documentation

core / init.control.monad

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

Identical to has_bind.and_then, but it is not inlined.

Equations