Documentation

Lean.AddDecl

source
opaque Lean.debug.skipKernelTC :
Lean.Option Bool
source
def Lean.Environment.addDecl (env : Lean.Environment) (opts : Lean.Options) (decl : Lean.Declaration) (cancelTk? : optParam (Option IO.CancelToken) none) :
Except Lean.KernelException Lean.Environment
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Environment.addAndCompile (env : Lean.Environment) (opts : Lean.Options) (decl : Lean.Declaration) (cancelTk? : optParam (Option IO.CancelToken) none) :
Except Lean.KernelException Lean.Environment
Equations
  • env.addAndCompile opts decl cancelTk? = do let env ← env.addDecl opts decl cancelTk? env.compileDecl opts decl
source
def Lean.addDecl (decl : Lean.Declaration) :
Lean.CoreM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.addAndCompile (decl : Lean.Declaration) :
Lean.CoreM Unit
Equations