def Id (type : Type u) : Type u

@[always_inline]

instance Id.instMonad : Monad Id

Equations

• Id.instMonad = Monad.mk

def Id.hasBind : Bind Id

Equations

• Id.hasBind = inferInstance

@[inline]

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

Equations

• x.run = x

instance Id.instOfNat {α : Type u_1} {n : Nat} [OfNat α n] : OfNat (Id α) n

Equations

• Id.instOfNat = inferInstanceAs (OfNat α n)