def
Lean.Kernel.Environment.addDecl
(env : Environment)
(opts : Options)
(decl : Declaration)
(cancelTk? : Option IO.CancelToken := none)
:
Adds given declaration to the environment, respecting debug.skipKernelTC
.
Equations
Instances For
@[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)
:
Equations
Instances For
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
Instances For
Checks whether the declaration was originally declared as a theorem; see also
Lean.getOriginalConstKind?
. Returns false
if the declaration was not found.