def Id (type : Type u) : Type u

Equations

• Id type = type

@[always_inline]

instance Id.instMonadId : Monad Id

Equations

• Id.instMonadId = Monad.mk

def Id.hasBind : Bind Id

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} [OfNat α n] : OfNat (Id α) n

Equations

• Id.instOfNatId = inferInstanceAs (OfNat α n)