Documentation

Init.SizeOf

SizeOf #

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.

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

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

    Equations
    Instances For
      @[instance 100]
      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} [SizeOf α] :
      SizeOf (Unitα)
      Equations
      • instSizeOfForallUnit = { sizeOf := fun (f : Unitα) => sizeOf (f ()) }
      @[simp]
      theorem sizeOf_thunk {α : Sort u_1} [SizeOf α] (f : Unitα) :
      @[simp]
      theorem Unit.sizeOf (u : Unit) :
      sizeOf u = 1
      @[simp]
      theorem Bool.sizeOf_eq_one (b : Bool) :
      sizeOf b = 1
      noncomputable def Lean.Name.sizeOf :

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

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