Documentation

Lean.AddDecl

source
def Lean.Kernel.Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) (cancelTk? : Option IO.CancelToken := none) :
Except Exception Environment

Adds given declaration to the environment, respecting debug.skipKernelTC.

Equations
  • One or more equations did not get rendered due to their size.
source
@[deprecated "use `Lean.addDecl` instead to ensure new namespaces are registered" (since := "2024-12-03")]
def Lean.Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration) (cancelTk? : Option IO.CancelToken := none) :
Except Kernel.Exception Environment
Equations
source
def Lean.getOriginalConstKind? (env : Environment) (declName : Name) :
Option ConstantKind

Returns the kind of the declaration as originally declared instead of as exported. This information is stored by Lean.addDecl and may be inaccurate if that function was circumvented. Returns none if the declaration was not found.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.wasOriginallyTheorem (env : Environment) (declName : Name) :
Bool

Checks whether the declaration was originally declared as a theorem; see also Lean.getOriginalConstKind?. Returns false if the declaration was not found.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.addDecl (decl : Declaration) :
CoreM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.addDecl.doAdd (decl : Declaration) :
CoreM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.addDecl.addAsAxiom (decl : Declaration) :
CoreM PUnit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.addAndCompile (decl : Declaration) :
CoreM Unit
Equations