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
• binders : Syntax
• numSectionVars : Nat
• type : Expr
• value : Expr
• termination : TerminationHints

@[implicit_reducible]

instance Lean.Elab.instInhabitedPreDefinition : Inhabited PreDefinition

def Lean.Elab.instInhabitedPreDefinition.default : 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.addPreDefDocs (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) : TermElabM Unit

Adds the docstring, if relevant.

This should be done just after compilation so the predefinition can be executed in examples in its docstring. If code generation will not occur, then it should be done after adding the declaration to the environment.

def Lean.Elab.addPreDefInfo (preDef : PreDefinition) : TermElabM Unit

Adds constant info to the definition name. This should occur after executing post-compilation attributes, in case they have an effect on hovers.

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

def Lean.Elab.addNonRec (docCtx : LocalContext × LocalInstances) (preDef : PreDefinition) (applyAttrAfterCompilation : Bool := true) (all : List Name := [preDef.declName]) (cacheProofs : Bool := true) (cleanupValue isRecursive : 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 (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition) (safety : DefinitionSafety := DefinitionSafety.unsafe) : TermElabM Unit

def Lean.Elab.addAndCompilePartialRec (docCtx : LocalContext × LocalInstances) (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)