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

Equations

• env.addDecl opts decl = 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