def Lean.Compiler.LCNF.init : Pass

Equations

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

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

Equations

• Lean.Compiler.LCNF.trace phase = { occurrence := 0, phase := phase, phaseOut := phase, phaseInv := ⋯, name := `trace, run := pure }

def Lean.Compiler.LCNF.saveBase : Pass

Equations

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

def Lean.Compiler.LCNF.saveMono : Pass

Equations

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

def Lean.Compiler.LCNF.builtinPassManager : PassManager

Equations

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

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

Equations

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

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

def Lean.Compiler.LCNF.getPassManager : CoreM 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 : Name) : CoreM Unit

Equations

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