mathlib documentation

core / init.control.id

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

id β

Equations

id_bind x f = f x

@[protected, instance]

def id.monad :

Equations

id.monad = monad.mk

@[protected, instance]

def id.monad_run :

monad_run id id

Equations

id.monad_run = {run := id}