Documentation

Lean.Elab.PreDefinition.Basic

structure Lean.Elab.PreDefinition:

Type

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

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

instance Lean.Elab.instInhabitedPreDefinition:

Inhabited 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)

Equations

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

def Lean.Elab.levelMVarToParamPreDecls (preDefs : Array Lean.Elab.PreDefinition) :

Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)

Equations

Lean.Elab.levelMVarToParamPreDecls preDefs = StateRefT'.run' (Lean.Elab.levelMVarToParamPreDeclsAux preDefs) 1

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

Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)

Equations

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

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

Lean.Elab.TermElabM Unit

Equations

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

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

Lean.MetaM Lean.Elab.PreDefinition

Equations

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

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

Lean.MetaM Unit

Equations

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

def Lean.Elab.addAndCompileNonRec (preDef : Lean.Elab.PreDefinition) (all : optParam (List Lean.Name) [preDef.declName]) :

Lean.Elab.TermElabM Unit

Equations

Lean.Elab.addAndCompileNonRec preDef all = Lean.Elab.addNonRecAux preDef true all true

def Lean.Elab.addNonRec (preDef : Lean.Elab.PreDefinition) (applyAttrAfterCompilation : optParam Bool true) (all : optParam (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.

Equations

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

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 : optParam 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 (recFnName : Lean.Name) (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

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