Documentation

Init.SizeOf

SizeOf #

source
class SizeOf (α : Sort u) :
Sort (max 1 u)

SizeOf is a typeclass automatically derived for every inductive type, which equips the type with a "size" function to Nat. The default instance defines each constructor to be 1 plus the sum of the sizes of all the constructor fields.

This is used for proofs by well-founded induction, since every field of the constructor has a smaller size than the constructor itself, and in many cases this will suffice to do the proof that a recursive function is only called on smaller values. If the default proof strategy fails, it is recommended to supply a custom size measure using the termination_by argument on the function definition.

  • sizeOf : α → Nat

    The "size" of an element, a natural number which decreases on fields of each inductive type.

Instances

    Declare SizeOf instances and theorems for types declared before SizeOf. From now on, the inductive compiler will automatically generate SizeOf instances and theorems.

    source
    def default.sizeOf (α : Sort u) :
    α → Nat

    Every type α has a default SizeOf instance that just returns 0 for every element of α.

    Equations
    Instances For
      source
      @[instance 100]
      instance instSizeOfDefault (α : Sort u) :
      SizeOf α

      Every type α has a low priority default SizeOf instance that just returns 0 for every element of α.

      source
      @[simp]
      theorem sizeOf_default {α : Sort u_1} (n : α) :
      sizeOf n = 0
      source
      instance instSizeOfNat :
      SizeOf Nat
      source
      @[simp]
      theorem sizeOf_nat (n : Nat) :
      sizeOf n = n
      source
      instance instSizeOfForallUnit {α : Sort u_1} [SizeOf α] :
      SizeOf (Unit → α)
      source
      @[simp]
      theorem sizeOf_thunk {α : Sort u_1} [SizeOf α] (f : Unit → α) :
      sizeOf f = sizeOf (f ())
      source
      @[simp]
      theorem Unit.sizeOf (u : Unit) :
      sizeOf u = 1
      source
      @[simp]
      theorem Bool.sizeOf_eq_one (b : Bool) :
      sizeOf b = 1
      source
      noncomputable def Lean.Name.sizeOf :
      Lean.Name → Nat

      We manually define the Lean.Name instance because we use an opaque function for computing the hashcode field.

      Instances For
        source
        noncomputable instance Lean.instSizeOfName :
        SizeOf Lean.Name
        Equations
        source
        @[simp]
        theorem Lean.Name.anonymous.sizeOf_spec :
        sizeOf Lean.Name.anonymous = 1
        source
        @[simp]
        theorem Lean.Name.str.sizeOf_spec (p : Lean.Name) (s : String) :
        sizeOf (p.str s) = 1 + sizeOf p + sizeOf s
        source
        @[simp]
        theorem Lean.Name.num.sizeOf_spec (p : Lean.Name) (n : Nat) :
        sizeOf (p.num n) = 1 + sizeOf p + sizeOf n