opaque Lean.debug.skipKernelTC : Lean.Option Bool

def Lean.Environment.addDecl (env : Lean.Environment) (opts : Lean.Options) (decl : Lean.Declaration) : Except Lean.KernelException Lean.Environment

Equations

• env.addDecl opts decl = if Lean.Option.get opts Lean.debug.skipKernelTC = true then env.addDeclWithoutChecking decl else env.addDeclCore (Lean.Core.getMaxHeartbeats opts).toUSize decl

def Lean.Environment.addAndCompile (env : Lean.Environment) (opts : Lean.Options) (decl : Lean.Declaration) : Except Lean.KernelException Lean.Environment

Equations

• env.addAndCompile opts decl = do let env ← env.addDecl opts decl env.compileDecl opts decl

def Lean.addDecl (decl : Lean.Declaration) : Lean.CoreM Unit

Equations

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

def Lean.addAndCompile (decl : Lean.Declaration) : Lean.CoreM Unit

Equations

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