Documentation

Init.SizeOf

class SizeOf (α : Sort u) :

Sort (max 1 u)

sizeOf : α → Nat

Instances

def default.sizeOf (α : Sort u) :

α → Nat

Equations

default.sizeOf α _fun_discr = match _fun_discr with | x => 0

instance instSizeOf (α : Sort u) :

Equations

instSizeOf α = { sizeOf := default.sizeOf α }

@[simp]

theorem sizeOf_default {α : Sort u_1} (n : α) :

instance instSizeOfNat:

Equations

instSizeOfNat = { sizeOf := fun n => n }

@[simp]

theorem sizeOf_nat (n : Nat) :

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 → α) :

sizeOf f = sizeOf (f ())

@[simp]

theorem Unit.sizeOf (u : Unit) :

@[simp]

theorem Bool.sizeOf_eq_one (b : Bool) :

noncomputable def Lean.Name.sizeOf:

Lean.Name → Nat

Equations

Lean.Name.sizeOf Lean.Name.anonymous = 1
Lean.Name.sizeOf (Lean.Name.str p s a) = 1 + Lean.Name.sizeOf p + sizeOf s
Lean.Name.sizeOf (Lean.Name.num p n a) = 1 + Lean.Name.sizeOf p + sizeOf n

noncomputable instance Lean.instSizeOfName:

SizeOf Lean.Name

Equations

Lean.instSizeOfName = { sizeOf := fun n => Lean.Name.sizeOf n }

@[simp]

theorem Lean.Name.anonymous.sizeOf_spec:

sizeOf Lean.Name.anonymous = 1

@[simp]

theorem Lean.Name.str.sizeOf_spec (p : Lean.Name) (s : String) (h : UInt64) :

sizeOf (Lean.Name.str p s h) = 1 + sizeOf p + sizeOf s

@[simp]

theorem Lean.Name.num.sizeOf_spec (p : Lean.Name) (n : Nat) (h : UInt64) :

sizeOf (Lean.Name.num p n h) = 1 + sizeOf p + sizeOf n