# Documentation

Lean.Meta.SizeOf

def Lean.Meta.mkSizeOfFn (recName : Lean.Name) (declName : Lean.Name) :

Create a "sizeOf" function with name declName using the recursor recName.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.mkSizeOfFns (typeName : Lean.Name) :

Create sizeOf functions for all inductive datatypes in the mutual inductive declaration containing typeName The resulting array contains the generated functions names. The NameMap maps recursor names into the generated function names. There is a function for each element of the mutual inductive declaration, and for auxiliary recursors for nested inductive types.

Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.

# SizeOf spec theorem for nested inductive types #

Instances For
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.