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.snapshotEnvLinterOptions (declName : Name) : CoreM Unit

Saves the state of Lean.Options associated with environment linters into envLinterSnapshotExt

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

• Lean.addDecl decl forceExpose = do Lean.addDeclCore✝ decl forceExpose discard (List.mapM Lean.snapshotEnvLinterOptions decl.getTopLevelNames)

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

Equations

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