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

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

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

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

SizeOf spec theorem for nested inductive types

structure Lean.Meta.SizeOfSpecNested.Context : Type

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

@[inline, reducible]

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

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

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

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

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

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

opaque Lean.Meta.genSizeOf : Lean.Option Bool

opaque Lean.Meta.genSizeOfSpec : Lean.Option Bool

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