# Documentation

Lean.Compiler.LCNF.PassManager

Equations
• Lean.Compiler.LCNF.instDecidableLtPhaseInstLTPhase =
Equations
• Lean.Compiler.LCNF.instDecidableLePhaseInstLEPhase =
• Which occurrence of the pass in the pipeline this is. Some passes, like simp, can occur multiple times in the pipeline. For most passes this value does not matter.

occurrence : Nat
• Which phase this Pass is supposed to run in

• Resulting phase.

• phaseInv : autoParam (phaseOut phase) _auto✝
• The name of the Pass

name : Lean.Name
• The actual pass function, operating on the Decls.

A single compiler Pass, consisting of the actual pass function operating on the Decls as well as meta information.

Instances For
• When the installer is run this function will receive a list of all current Passes and return a new one, this can modify the list (and the Passes contained within) in any way it wants.

install :

Can be used to install, remove, replace etc. passes by tagging a declaration of type PassInstaller with the cpass attribute.

Instances For
Equations
• passes :

The PassManager used to store all Passes that will be run within pipeline.

Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• = { install := fun passes => pure (passes ++ passesNew) }
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.