- reduce: Lean.Meta.ACLt.ReduceMode
- reduceSimpleOnly: Lean.Meta.ACLt.ReduceMode
- none: Lean.Meta.ACLt.ReduceMode
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.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
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.