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

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

Instances For

source
def Lean.Compiler.LCNF.Pass.checkMeta :
Pass
Equations

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

Instances For

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

- Lean.Compiler.LCNF.Pass.trace phase = { phase := phase, phaseInv := ⋯, name := `trace, run := pure }

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
opaque Lean.Compiler.LCNF.passManagerExt :
PersistentEnvExtension Name (Name × PassManager) (List Name × PassManager)
source
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

Instances For

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

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

Instances For