HepLean 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? : Option IO.CancelToken := none) :
Except Lean.KernelException Lean.Environment
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Environment.addAndCompile (env : Lean.Environment) (opts : Lean.Options) (decl : Lean.Declaration) (cancelTk? : 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
    Instances For
      source
      def Lean.addDecl (decl : Lean.Declaration) :
      Lean.CoreM Unit
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.addAndCompile (decl : Lean.Declaration) :
        Lean.CoreM Unit
        Equations
        Instances For