HepLean Documentation

Lean.Compiler.IR

source
opaque Lean.IR.compiler.reuse :
Lean.Option Bool
source
@[export lean_ir_compile]
def Lean.IR.compile (env : Lean.Environment) (opts : Lean.Options) (decls : Array Lean.IR.Decl) :
Lean.IR.Log × Except String Lean.Environment
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.IR.addBoxedVersionAux (decl : Lean.IR.Decl) :
    Lean.IR.CompilerM Unit
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[export lean_ir_add_boxed_version]
      def Lean.IR.addBoxedVersion (env : Lean.Environment) (decl : Lean.IR.Decl) :
      Except String Lean.Environment
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For