feat: add pre simp lemmas for if-then-else terms See new test for example that takes exponential time without new simp theorems. TODO: replace auxiliary theorems with simprocs as soon as we implement them.
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.