experiment: whnf optimization in cbv for Decidable.decide

[wkrozowski]

No description provided.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for 1b1cb3d against c6f4fa8 are in! @wkrozowski

• ✅ build//instructions: -359.7M (-0.00%)

Large changes (1✅)

• ✅ cbv tactic (Eratosthenes' sieve)//instructions: -13.7G (-21.80%)

Small changes (4🟥)

• 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//bytes .ilean: +5kiB (+19.87%)
• 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//bytes .olean.private: +61kiB (+13.44%)
• 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//bytes .olean.server: +624B (+20.47%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Meta.Tactic.Cbv.ControlFlow//instructions: +663.9M (+9.36%) (reduced significance based on *//lines)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c6f4fa8678132215f01679518b015c3c464c6e25 --onto 6ca23a7b8bee57152110ce500ce795148707d4ed. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-13 18:35:48)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c6f4fa8678132215f01679518b015c3c464c6e25 --onto 9da8f5dce42832b8411d58446653f3640a94a6e3. You can force reference manual CI using the force-manual-ci label. (2026-02-13 18:35:50)