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.
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.
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.