mathlib documentation

core.init.control.id

def id_bind {α β : Type u} :
α → (α → id β)id β

Equations
@[instance]
def id.monad  :

Equations
@[instance]

Equations