def Lean.Compiler.LCNF.init : Lean.Compiler.LCNF.Pass

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.trace (phase : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) : Lean.Compiler.LCNF.Pass

Equations

• Lean.Compiler.LCNF.trace phase = Lean.Compiler.LCNF.Pass.mk 0 phase phase `trace pure

def Lean.Compiler.LCNF.saveBase : Lean.Compiler.LCNF.Pass

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.saveMono : Lean.Compiler.LCNF.Pass

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.builtinPassManager : Lean.Compiler.LCNF.PassManager

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.runImportedDecls (importedDeclNames : Array (Array Lean.Name)) : Lean.CoreM Lean.Compiler.LCNF.PassManager

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.Compiler.LCNF.passManagerExt : Lean.PersistentEnvExtension Lean.Name (Lean.Name × Lean.Compiler.LCNF.PassManager) (List Lean.Name × Lean.Compiler.LCNF.PassManager)

def Lean.Compiler.LCNF.getPassManager : Lean.CoreM Lean.Compiler.LCNF.PassManager

Equations

• Lean.Compiler.LCNF.getPassManager = do let __do_lift ← Lean.getEnv pure (Lean.PersistentEnvExtension.getState Lean.Compiler.LCNF.passManagerExt __do_lift).snd

def Lean.Compiler.LCNF.addPass (declName : Lean.Name) : Lean.CoreM Unit

Equations

• One or more equations did not get rendered due to their size.