structure Lean.Elab.PreDefinition : Type

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

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

instance Lean.Elab.instInhabitedPreDefinition : Inhabited Lean.Elab.PreDefinition

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

Equations

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

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

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

def Lean.Elab.levelMVarToParamTypesPreDecls (preDefs : Array Lean.Elab.PreDefinition) : Lean.Elab.TermElabM (Array Lean.Elab.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 Lean.Elab.PreDefinition) (scopeLevelNames allUserLevelNames : List Lean.Name) : Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)

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

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

def Lean.Elab.addAsAxiom (preDef : Lean.Elab.PreDefinition) : Lean.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.addAndCompileNonRec (preDef : Lean.Elab.PreDefinition) (all : List Lean.Name := [preDef.declName]) : Lean.Elab.TermElabM Unit

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

Equations

• Lean.Elab.addNonRec preDef applyAttrAfterCompilation all = Lean.Elab.addNonRecAux✝ preDef false all applyAttrAfterCompilation

def Lean.Elab.eraseRecAppSyntaxExpr (e : Lean.Expr) : Lean.CoreM Lean.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 : Lean.Elab.PreDefinition) : Lean.CoreM Lean.Elab.PreDefinition

Equations

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

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

Equations

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

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

Equations

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

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

def Lean.Elab.checkCodomainsLevel (preDefs : Array Lean.Elab.PreDefinition) : Lean.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 Lean.Elab.PreDefinition) : Lean.CoreM (Array Lean.Elab.PreDefinition)