opaque Lean.Elab.cleanup.letToHave : Lean.Option Bool

structure Lean.Elab.PreDefinition : Type

A (potentially recursive) definition. The elaborator converts it into Kernel definitions using many different strategies.

• ref : Syntax
• kind : DefKind
• levelParams : List Name
• modifiers : Modifiers
• declName : Name
• type : Expr
• value : Expr
• termination : TerminationHints

instance Lean.Elab.instInhabitedPreDefinition : Inhabited PreDefinition

def Lean.Elab.PreDefinition.filterAttrs (preDef : PreDefinition) (p : Attribute → Bool) : PreDefinition

def Lean.Elab.instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition)

Applies Lean.instantiateMVars to the types of values of each predefinition.

def Lean.Elab.levelMVarToParamTypesPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition)

Applies Lean.Elab.Term.levelMVarToParam to the types of each predefinition.

def Lean.Elab.fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition)

def Lean.Elab.applyAttributesOf (preDefs : Array PreDefinition) (applicationTime : AttributeApplicationTime) : TermElabM Unit

def Lean.Elab.letToHaveValue (preDef : PreDefinition) : MetaM PreDefinition

Applies Meta.letToHave to the values of defs, instances, and abbrevs. Does not apply the transformation to values that are proofs, or to unsafe definitions.

def Lean.Elab.letToHaveType (preDef : PreDefinition) : MetaM PreDefinition

Applies Meta.letToHave to the type of the predef.

def Lean.Elab.abstractNestedProofs (preDef : PreDefinition) (cache : Bool := true) : MetaM PreDefinition

def Lean.Elab.addAsAxiom (preDef : PreDefinition) : MetaM Unit

Auxiliary method for (temporarily) adding pre definition as an axiom

opaque Lean.Elab.diagnostics.threshold.proofSize : Lean.Option Nat

def Lean.Elab.addAndCompileNonRec (preDef : PreDefinition) (all : List Name := [preDef.declName]) (cleanupValue : Bool := false) : TermElabM Unit

def Lean.Elab.addNonRec (preDef : PreDefinition) (applyAttrAfterCompilation : Bool := true) (all : List Name := [preDef.declName]) (cacheProofs : Bool := true) (cleanupValue : Bool := false) : TermElabM Unit

def Lean.Elab.eraseRecAppSyntaxExpr (e : Expr) : CoreM Expr

Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module to produce better error messages.

def Lean.Elab.eraseRecAppSyntax (preDef : PreDefinition) : CoreM PreDefinition

def Lean.Elab.addAndCompileUnsafe (preDefs : Array PreDefinition) (safety : DefinitionSafety := DefinitionSafety.unsafe) : TermElabM Unit

def Lean.Elab.addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit

def Lean.Elab.ensureNoRecFn (recFnNames : Array Name) (e : Expr) : MetaM Unit

def Lean.Elab.checkCodomainsLevel (preDefs : Array PreDefinition) : MetaM Unit

Checks that all codomains have the same level, throws an error otherwise.

def Lean.Elab.shareCommonPreDefs (preDefs : Array PreDefinition) : CoreM (Array PreDefinition)