# Documentation

Lean.Elab.PreDefinition.Basic

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

Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.fixLevelParams (preDefs : ) (scopeLevelNames : ) (allUserLevelNames : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.applyAttributesOf (preDefs : ) (applicationTime : Lean.AttributeApplicationTime) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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

Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.addNonRec (preDef : Lean.Elab.PreDefinition) (applyAttrAfterCompilation : ) (all : optParam () [preDef.declName]) :
Equations

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.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Elab.ensureNoRecFn (recFnName : Lean.Name) (e : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.