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.

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.

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.

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