Documentation
Lean
.
Compiler
.
IR
Search
return to top
source
Imports
Lean.Compiler.IR.AddExtern
Lean.Compiler.IR.Basic
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.SimpleGroundExpr
Lean.Compiler.IR.Sorry
Lean.Compiler.IR.ToIR
Lean.Compiler.IR.ToIRType
Lean.Compiler.IR.Toposort
Lean.Compiler.IR.UnboxResult
Imported by
Lean
.
IR
.
compile
source
def
Lean
.
IR
.
compile
(
decls
:
Array
Decl
)
:
CompilerM
(
Array
Decl
)
Equations
One or more equations did not get rendered due to their size.
Instances For