Documentation

Lean.Meta.ACLt

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.
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.