mathlib documentation

core / init.control.id

def id_bind {α β : Type u} (x : α) (f : α → id β) :
id β
Equations
@[instance]
def id.monad  :
Equations
@[instance]
Equations