Documentation

Init.SizeOf

class SizeOf (α : Sort u) :
Sort (max 1 u)
  • sizeOf : αNat
Instances
def default.sizeOf (α : Sort u) :
αNat
Equations
instance instSizeOf (α : Sort u) :
Equations
@[simp]
theorem sizeOf_default {α : Sort u_1} (n : α) :
sizeOf n = 0
Equations
@[simp]
theorem sizeOf_nat (n : Nat) :
sizeOf n = n
instance instSizeOfForAllUnit {α : Sort u_1} [inst : SizeOf α] :
SizeOf (Unitα)
Equations
  • instSizeOfForAllUnit = { sizeOf := fun f => sizeOf (f ()) }
@[simp]
theorem sizeOf_thunk {α : Sort u_1} [inst : SizeOf α] (f : Unitα) :
@[simp]
theorem Unit.sizeOf (u : Unit) :
sizeOf u = 1
@[simp]
theorem Bool.sizeOf_eq_one (b : Bool) :
sizeOf b = 1
noncomputable instance Lean.instSizeOfName :
Equations
@[simp]
@[simp]
theorem Lean.Name.num.sizeOf_spec (p : Lean.Name) (n : Nat) (h : UInt64) :