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.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 a ← Lean.getEnv pure (Lean.PersistentEnvExtension.getState Lean.Compiler.LCNF.passManagerExt a).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.