fix: mark `Grind.nestedDecidable` as an abbreviation This PR fixes a performance issue where proof terms produced by `grind` could trigger kernel deterministic timeouts. `grind` canonicalizes nested `Decidable` instances under the identity wrapper `Grind.nestedDecidable`, leaving the kernel to check `t =?= Grind.nestedDecidable t`. The kernel does not see the `[reducible]` attribute, and its lazy-delta heuristic unfolded `t` instead of the wrapper. When `t` is an instance such as `UInt32.decLe` applied to a symbolic argument and a large literal (e.g., `97 ≤ c.val + 4294967264` coming from `Char`/`UInt32` wraparound), the check descended through `BitVec` and `Fin` into `Nat.ble` on a `2^32`-sized literal with a free variable inside, where the fast numeral path does not apply, and effectively never terminated. Marking `nestedDecidable` as an abbreviation stores the `abbrev` reducibility hint in the declaration itself, which the kernel does honor, so the wrapper side is unfolded first and the check succeeds immediately. The `unfoldReducible` preprocessor now treats `Grind.nestedDecidable` as a `grind` gadget that must not be unfolded: like `Grind.EqMatch` and `Grind.MatchCond`, it is an `abbrev` that must survive until the corresponding propagators consume it. Reported by Paul Reichert.
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.