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

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 : 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.

Equations

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

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

Equations

• Lean.Meta.mkSizeOfSpecLemmaName ctorName = ctorName ++ `sizeOf_spec

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

Equations

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

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

@[reducible, inline]

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

Equations

• Lean.Meta.SizeOfSpecNested.M = ReaderT Lean.Meta.SizeOfSpecNested.Context Lean.MetaM

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

opaque Lean.Meta.genSizeOf : Lean.Option Bool

opaque Lean.Meta.genSizeOfSpec : Lean.Option Bool

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

Equations

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