fix: if-then-else split + normalization issue This PR fixes an issue in the `grind` tactic when case splitting on if-then-else expressions. It adds a new marker gadget that prevents `grind` for re-normalizing the condition `c` of an if-then-else expression. Without this marker, the negated condition `¬c` might be rewritten into an alternative form `c'`, which `grind` may not recognize as equivalent to `¬c`. As a result, `grind` could fail to propagate that `if c then a else b` simplifies to `b` in the `¬c` branch.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).