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.

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

• env.addDecl opts decl cancelTk? = Lean.Environment.addDeclAux✝ env opts decl cancelTk?

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.

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.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.addAndCompile decl = do Lean.addDecl decl Lean.compileDecl decl