## Equations

- One or more equations did not get rendered due to their size.

## Instances For

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

- Lean.Meta.ACLt.main a b mode = Lean.Meta.ACLt.main.lt mode a b

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

- Lean.Meta.ACLt.main.someChildGe mode a b = do let __do_lift ← Lean.Meta.ACLt.main.allChildrenLt mode a b pure !__do_lift

## Instances For

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