- ref : Lean.Syntax
- kind : Lean.Elab.DefKind
- modifiers : Lean.Elab.Modifiers
- declName : Lake.Name
- type : Lean.Expr
- value : Lean.Expr
A (potentially recursive) definition. The elaborator converts it into Kernel definitions using many different strategies.
Instances For
Instances For
Instances For
def
Lean.Elab.fixLevelParams
(preDefs : Array Lean.Elab.PreDefinition)
(scopeLevelNames : List Lake.Name)
(allUserLevelNames : List Lake.Name)
:
Instances For
def
Lean.Elab.applyAttributesOf
(preDefs : Array Lean.Elab.PreDefinition)
(applicationTime : Lean.AttributeApplicationTime)
:
Instances For
Instances For
Auxiliary method for (temporarily) adding pre definition as an axiom
Instances For
def
Lean.Elab.addAndCompileNonRec
(preDef : Lean.Elab.PreDefinition)
(all : optParam (List Lake.Name) [preDef.declName])
:
Instances For
def
Lean.Elab.addNonRec
(preDef : Lean.Elab.PreDefinition)
(applyAttrAfterCompilation : optParam Bool true)
(all : optParam (List Lake.Name) [preDef.declName])
:
Instances For
Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module to produce better error messages.
Instances For
Instances For
def
Lean.Elab.addAndCompileUnsafe
(preDefs : Array Lean.Elab.PreDefinition)
(safety : optParam Lean.DefinitionSafety Lean.DefinitionSafety.unsafe)
: