Documentation

Init.SizeOfLemmas

@[simp]
theorem Fin.sizeOf {n : Nat} (a : Fin n) :
sizeOf a = a + 1
@[simp]
theorem UInt8.sizeOf (a : UInt8) :
sizeOf a = a.toNat + 2
@[simp]
theorem UInt16.sizeOf (a : UInt16) :
sizeOf a = a.toNat + 2
@[simp]
theorem UInt32.sizeOf (a : UInt32) :
sizeOf a = a.toNat + 2
@[simp]
theorem UInt64.sizeOf (a : UInt64) :
sizeOf a = a.toNat + 2
@[simp]
theorem USize.sizeOf (a : USize) :
sizeOf a = a.toNat + 2
@[simp]
theorem Char.sizeOf (a : Char) :
sizeOf a = a.toNat + 3
@[simp]
theorem Subtype.sizeOf {α : Sort u_1} {p : αProp} (s : Subtype p) :
sizeOf s = sizeOf s.val + 1