Equations
Instances For
Applies Lean.instantiateMVars
to the types of values of each predefinition.
Equations
Instances For
Applies Lean.Elab.Term.levelMVarToParam
to the types of each predefinition.
Equations
Instances For
def
Lean.Elab.fixLevelParams
(preDefs : Array PreDefinition)
(scopeLevelNames allUserLevelNames : List Name)
:
Equations
Instances For
def
Lean.Elab.applyAttributesOf
(preDefs : Array PreDefinition)
(applicationTime : AttributeApplicationTime)
:
Equations
Instances For
Equations
Instances For
Auxiliary method for (temporarily) adding pre definition as an axiom
Equations
Instances For
Equations
Instances For
Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module to produce better error messages.
Equations
Instances For
Equations
Instances For
def
Lean.Elab.addAndCompileUnsafe
(preDefs : Array PreDefinition)
(safety : DefinitionSafety := DefinitionSafety.unsafe)
:
Equations
Instances For
Equations
Instances For
Checks that all codomains have the same level, throws an error otherwise.