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.

@[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

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.

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.

opaque Lean.warn.sorry : Lean.Option Bool

If warn.sorry is set to true, then, so long as the message log does not already have any errors, declarations with sorryAx generate the "declaration uses 'sorry'" warning.

def Lean.addDecl (decl : Declaration) : CoreM Unit

def Lean.addDecl.doAdd (decl : Declaration) : CoreM Unit

def Lean.addDecl.addAsAxiom (decl : Declaration) : CoreM PUnit

def Lean.addAndCompile (decl : Declaration) : CoreM Unit