Documentation

Lean.Compiler.LCNF.PassManager

Equations
  • Lean.Compiler.LCNF.instDecidableLtPhase = p1.toNat.decLt p2.toNat
Equations
  • Lean.Compiler.LCNF.instDecidableLePhase = p1.toNat.decLe p2.toNat

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

Instances For
    theorem Lean.Compiler.LCNF.Pass.phaseInv (self : Lean.Compiler.LCNF.Pass) :
    self.phaseOut self.phase
    Equations
    • One or more equations did not get rendered due to their size.

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

    Instances For

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

      Instances For
        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.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For