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.

Instances For

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

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

Instances For

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.

Instances For

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