fix: make cbv_opaque take precedence over cbv_eval

[wkrozowski]

This PR makes @[cbv_opaque] unconditionally block all evaluation of a constant
by cbv, including @[cbv_eval] rewrite rules. Previously, @[cbv_eval] could
bypass @[cbv_opaque], and for bare constants (not applications), isOpaqueConst
could fall through to handleConst which would unfold the definition body.

The intended usage pattern is now: mark subterm-producing functions (like
DHashMap.insert) as @[cbv_opaque] to prevent unfolding, and provide
@[cbv_eval] theorems on the consuming function (like DHashMap.contains)
which pattern-matches against the opaque subterms.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for 00a809e against a32173e are in. There are no significant changes. @wkrozowski

• ✅ build//instructions: -672.1M (-0.01%)

Small changes (1✅, 1🟥)

• ✅ build/module/Lean.Meta.Tactic.Cbv.Main//instructions: -19.9M (-0.15%)
• 🟥 elab/cbv_leroy//instructions: +103.0M (+0.21%)

[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 a32173e6f63ee8851d3a08dfc5611fc0e96ca8c0 --onto e8048291010c815d0d30926924e7ad7afc18b1c0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-13 14:27:44)

[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 a32173e6f63ee8851d3a08dfc5611fc0e96ca8c0 --onto e6d9220eee278116b0bd28f9ec19388fdc690180. You can force reference manual CI using the force-manual-ci label. (2026-03-13 14:27:46)