- sizeOf : α → Nat
The "size" of an element, a natural number which decreases on fields of each inductive type.
SizeOf is a typeclass automatically derived for every inductive type,
which equips the type with a "size" function to
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.
We manually define the
Lean.Name instance because we use
an opaque function for computing the hashcode field.