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 : 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 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.Compiler.LCNF.passManagerExt.getState __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.