Documentation

Lean.Compiler.IR

source
opaque Lean.IR.compiler.reuse :
Lean.Option Bool
source
@[export lean_ir_compile]
def Lean.IR.compile (env : Environment) (opts : Options) (decls : Array Decl) :
Log × Except String Environment
Equations
    source
    def Lean.IR.addBoxedVersionAux (decl : Decl) :
    CompilerM Unit
    Equations
      source
      @[export lean_ir_add_boxed_version]
      def Lean.IR.addBoxedVersion (env : Environment) (decl : Decl) :
      Except String Environment
      Equations