Documentation

Lean.Meta.ACLt

Equations
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 instance 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
      Instances For
        Equations
        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 instance 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