Documentation

Init.SizeOfLemmas

@[simp]

theorem Fin.sizeOf {n : Nat} (a : Fin n) :

sizeOf a = a.val + 1

@[simp]

theorem UInt8.sizeOf (a : UInt8) :

sizeOf a = UInt8.toNat a + 2

@[simp]

theorem UInt16.sizeOf (a : UInt16) :

sizeOf a = UInt16.toNat a + 2

@[simp]

theorem UInt32.sizeOf (a : UInt32) :

sizeOf a = UInt32.toNat a + 2

@[simp]

theorem UInt64.sizeOf (a : UInt64) :

sizeOf a = UInt64.toNat a + 2

@[simp]

theorem USize.sizeOf (a : USize) :

sizeOf a = USize.toNat a + 2

@[simp]

theorem Char.sizeOf (a : Char) :

sizeOf a = Char.toNat a + 3

@[simp]

theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) :

sizeOf s = sizeOf s.val + 1