Documentation

Init.SizeOf

source
class SizeOf (α : Sort u) :
Sort (max 1 u)
  • sizeOf : α → Nat
Instances
source
def default.sizeOf (α : Sort u) :
α → Nat
Equations
source
instance instSizeOf (α : Sort u) :
SizeOf α
Equations
source
@[simp]
theorem sizeOf_default {α : Sort u_1} (n : α) :
sizeOf n = 0
source
instance instSizeOfNat :
SizeOf Nat
Equations
source
@[simp]
theorem sizeOf_nat (n : Nat) :
sizeOf n = n
source
noncomputable def Lean.Name.sizeOf :
Lean.Name → Nat
Equations
source
noncomputable instance instSizeOfName :
SizeOf Lean.Name
Equations