def Id (type : Type u) : Type u

Equations

• Id type = type

Instances For

• Id.finally
• Id.instLawfulMonad
• Id.instMonad
• Id.instOfNat
• Lake.instComputeHashBoolId
• Lake.instComputeHashStringId
• Lake.instMonadLiftTIdOfPure_lake
• instReprId_1
• instToStringId_1

@[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)