Documentation

Lean.Meta.SizeOf

source
def Lean.Meta.mkSizeOfFn (recName : Lean.Name) (declName : Lean.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.
source
def Lean.Meta.mkSizeOfFns (typeName : Lean.Name) :
Lean.MetaM (Array Lean.Name × Lean.NameMap 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.
source
def Lean.Meta.mkSizeOfSpecLemmaName (ctorName : Lean.Name) :
Lean.Name
Equations
source
def Lean.Meta.mkSizeOfSpecLemmaInstance (ctorApp : Lean.Expr) :
Lean.MetaM Lean.Expr
Equations
  • One or more equations did not get rendered due to their size.
source
structure Lean.Meta.SizeOfSpecNested.Context:
Type
source
@[inline]
abbrev Lean.Meta.SizeOfSpecNested.M (α : Type) :
Type
Equations
source
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.
source
def Lean.Meta.SizeOfSpecNested.throwFailed {α : Type} :
Lean.Meta.SizeOfSpecNested.M α
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
partial def Lean.Meta.SizeOfSpecNested.main.loop (lhs : Lean.Expr) (rhs : Lean.Expr) :
Lean.Meta.SizeOfSpecNested.M Lean.Expr
source
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.
source
opaque Lean.Meta.genSizeOf:
Lean.Option Bool
source
opaque Lean.Meta.genSizeOfSpec:
Lean.Option Bool
source
def Lean.Meta.mkSizeOfInstances (typeName : Lean.Name) :
Lean.MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.