Documentation

Init.Control.Id

noncomputable def Id (type : Type u) :

Type u

Equations

Id type = type

instance Id.instMonadId :

Equations

Id.instMonadId = Monad.mk

def Id.hasBind :

Equations

Id.hasBind = inferInstance

@[inline]

def Id.run {α : Type u_1} (x : Id α) :

α

Equations

Id.run x = x

instance Id.instOfNatId {α : Type u_1} {n : Nat} [inst : OfNat α n] :

OfNat (Id α) n

Equations

Id.instOfNatId = inferInstanceAs (OfNat α n)