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

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

def Lean.Meta.mkSizeOfFns (typeName : Name) : MetaM (Array Name × NameMap 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.

def Lean.Meta.mkSizeOfSpecLemmaName (ctorName : Name) : Name

def Lean.Meta.mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr

SizeOf spec theorem for nested inductive types

structure Lean.Meta.SizeOfSpecNested.Context : Type

• indInfo : InductiveVal
• sizeOfFns : Array Name
• ctorName : Name
• params : Array Expr
• localInsts : Array Expr
• recMap : NameMap Name

@[reducible, inline]

abbrev Lean.Meta.SizeOfSpecNested.M (α : Type) : Type

def Lean.Meta.SizeOfSpecNested.throwUnexpected {α : Type} (msg : MessageData) : M α

def Lean.Meta.SizeOfSpecNested.throwFailed {α : Type} : M α

def Lean.Meta.SizeOfSpecNested.main (lhs rhs : Expr) : M Expr

partial def Lean.Meta.SizeOfSpecNested.main.loop (lhs rhs : Expr) : M Expr

def Lean.Meta.SizeOfSpecNested.main.step (lhs rhs : Expr) : M Expr

opaque Lean.Meta.genSizeOf : Lean.Option Bool

opaque Lean.Meta.genSizeOfSpec : Lean.Option Bool

def Lean.Meta.mkSizeOfInstances (typeName : Name) : MetaM Unit