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.

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.

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.warnIfUsesSorry (decl : Declaration) : CoreM Unit

If the warn.sorry option is set to true and there are no errors in the log already, logs a warning if the declaration uses sorry.

Equations

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

def Lean.addDecl (decl : Declaration) (forceExpose : Bool := false) : CoreM Unit

Adds the given declaration to the environment's private scope, deriving a suitable presentation in the public scope if under the module system and if the declaration is not private. If forceExpose is true, exposes the declaration body, i.e. preserves the full representation in the public scope, independently of Environment.isExporting and even for theorems.

Equations

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

def Lean.addAndCompile (decl : Declaration) (logCompileErrors : Bool := true) : CoreM Unit

Equations

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