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

Equations

• Lean.Elab.instInhabitedPreDefinition = { default := Lean.Elab.instInhabitedPreDefinition.default }

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

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

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

Applies Meta.letToHave to the type of the predef.

Equations

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

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

Equations

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

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

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

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

• Lean.Elab.addAndCompileNonRec docCtx preDef all cleanupValue isRecursive = Lean.Elab.addNonRecAux✝ docCtx preDef true all true true cleanupValue isRecursive

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

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.addAndCompilePartialRec (docCtx : LocalContext × LocalInstances) (preDefs : Array PreDefinition) : TermElabM Unit

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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