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
    Instances For
      source
      def Lean.IR.addBoxedVersionAux (decl : Decl) :
      CompilerM Unit
      Equations
        Instances For
          source
          @[export lean_ir_add_boxed_version]
          def Lean.IR.addBoxedVersion (env : Environment) (decl : Decl) :
          Except String Environment
          Equations
            Instances For