mathlib3 documentation

core / init.control.id

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