Documentation

Lean.Meta.ACLt

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

    An AC-compatible ordering.

    Recall that an AC-compatible ordering if it is monotonic, well-founded, and total. Both KBO and LPO are AC-compatible. KBO is faster, but we do not cache the weight of each expression in Lean 4. Even if we did, we would need to have a weight where implicit instace arguments are ignored. So, we use a LPO-like term ordering.

    Remark: this method is used to implement ordered rewriting. We ignore implicit instance arguments to address an issue reported at issue #972.

    Remark: the order is not really total on terms since

    • We instance implicit arguments.
    • We ignore metadata.
    • We ignore universe parameterst at constants.
    Equations
    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
                    @[implemented_by Lean.Meta.ACLt.main]

                    An AC-compatible ordering.

                    Recall that an AC-compatible ordering if it is monotonic, well-founded, and total. Both KBO and LPO are AC-compatible. KBO is faster, but we do not cache the weight of each expression in Lean 4. Even if we did, we would need to have a weight where implicit instace arguments are ignored. So, we use a LPO-like term ordering.

                    Remark: this method is used to implement ordered rewriting. We ignore implicit instance arguments to address an issue reported at issue #972.

                    Remark: the order is not really total on terms since

                    • We instance implicit arguments.
                    • We ignore metadata.
                    • We ignore universe parameterst at constants.