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 = { occurrence := 0, phase := phase, phaseOut := phase, phaseInv := ⋯, name := `trace, run := 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 Lake.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 Lake.Name (Lake.Name × Lean.Compiler.LCNF.PassManager) (List Lake.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.Compiler.LCNF.passManagerExt.getState __do_lift).snd

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

Equations

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