chore: fix regression due to changes in previous commits The example was looping with the new `simp` reduction strategy. Here is the looping trace. ``` List.reverseAux (List.reverseAux as []) bs ==> rewrite using reverseAux_reverseAux List.reverseAux [] (List.reverseAux (List.reverseAux as []) bs) ==> unfold reverseAux List.reverseAux (List.reverseAux as []) bs ==> rewrite using reverseAux_reverseAux List.reverseAux [] (List.reverseAux (List.reverseAux as []) bs) ==> ... ```
This is the repository for Lean 4.
We provide nightly releases and have just begun regular stable point releases.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean.