Documentation
Lean
.
Compiler
.
IR
Search
return to top
source
Imports
Lean.Compiler.IR.AddExtern
Lean.Compiler.IR.Basic
Lean.Compiler.IR.Borrow
Lean.Compiler.IR.Boxing
Lean.Compiler.IR.Checker
Lean.Compiler.IR.CompilerM
Lean.Compiler.IR.ElimDeadVars
Lean.Compiler.IR.EmitC
Lean.Compiler.IR.EmitLLVM
Lean.Compiler.IR.ExpandResetReuse
Lean.Compiler.IR.Format
Lean.Compiler.IR.LLVMBindings
Lean.Compiler.IR.Meta
Lean.Compiler.IR.NormIds
Lean.Compiler.IR.PushProj
Lean.Compiler.IR.RC
Lean.Compiler.IR.ResetReuse
Lean.Compiler.IR.SimpCase
Lean.Compiler.IR.Sorry
Lean.Compiler.IR.ToIR
Lean.Compiler.IR.ToIRType
Lean.Compiler.IR.Toposort
Lean.Compiler.IR.UnboxResult
Imported by
Lean
.
IR
.
compiler
.
reuse
Lean
.
IR
.
compile
source
opaque
Lean
.
IR
.
compiler
.
reuse
:
Lean.Option
Bool
source
def
Lean
.
IR
.
compile
(
decls
:
Array
Decl
)
:
CompilerM
(
Array
Decl
)
Equations
Instances For