opaque Lean.debug.skipKernelTC : Lean.Option Bool

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

Equations

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