[arthur-adjedj]

This PR avoids Except.bind and OptionT.bind from always reducing their continuations during definitional equality. This reduction can quickly become expensive, despite often not being useful. This performance regression is avoided by making these declarations be marked as abbreviations for lazy-delta reduction. Comparing #15447's mwe.lean example shows a measurable performance gain:

	nightly-2026-11-07	This PR
Wall time	2.5 min	620.5 ms
Memory	5.4 GiB	447.0 MiB

Closes #15447

[arthur-adjedj]

!bench

[leanprover-radar]

Benchmark results for a838dab against d4cada4 are in. There are significant results. @arthur-adjedj

• 🟥 build//instructions: +72.4M (+0.00%)

Large changes (40✅)

• ✅ compiled/incr_header_save//maxrss: -78MiB (-4.19%)
• ✅ elab/big_beq//maxrss: -104MiB (-6.03%)
• ✅ elab/big_beq_rec//maxrss: -103MiB (-5.94%)
• ✅ elab/big_deceq//maxrss: -104MiB (-6.07%)
• ✅ elab/big_deceq_rec//maxrss: -104MiB (-6.04%)
• ✅ elab/big_match//maxrss: -104MiB (-5.92%)
• ✅ elab/big_match_nat//maxrss: -104MiB (-6.08%)
• ✅ elab/big_match_nat_split//maxrss: -104MiB (-5.98%)
• ✅ elab/big_match_partial//maxrss: -104MiB (-5.89%)
• ✅ elab/bitvec_zero_counts//maxrss: -26MiB (-2.90%)
• ✅ elab/bv_decide_incremental//maxrss: -104MiB (-5.23%)
• ✅ elab/cbv_decide//maxrss: -108MiB (-5.99%)
• ✅ elab/cbv_merge_sort//maxrss: -107MiB (-5.97%)
• ✅ elab/charactersIn//maxrss: -27MiB (-2.92%)
• ✅ elab/delayed_assign//maxrss: -107MiB (-6.22%)
• ✅ elab/delayed_lift//maxrss: -109MiB (-6.28%)
• ✅ elab/delayed_sharing//maxrss: -111MiB (-6.47%)
• ✅ elab/grind_cases_next//maxrss: -118MiB (-6.55%)
• ✅ elab/let_to_have_chain//maxrss: -109MiB (-6.36%)
• ✅ elab/let_to_have_closed_body//maxrss: -111MiB (-6.43%)
• and 20 more

Medium changes (7✅, 2🟥)

• 🟥 compiled/rbmap_checkpoint//task-clock: +320ms (+23.31%)
• 🟥 compiled/rbmap_checkpoint//wall-clock: +330ms (+23.66%)
• ✅ elab/cbv_divisors//maxrss: -105MiB (-6.06%)
• ✅ elab/inferTypeCache//maxrss: -31MiB (-3.47%)
• ✅ elab/irDeclLookup//maxrss: -32MiB (-3.53%)
• ✅ elab/realizations//maxrss: -108MiB (-2.63%)
• ✅ elab/reduceMatch//maxrss: -109MiB (-6.25%)
• ✅ elab/stringLiteralDefEq//maxrss: -30MiB (-3.16%)
• ✅ elab/workspaceSymbols//maxrss: -21MiB (-2.30%)

Small changes (16✅, 9🟥)

• 🟥 compiled/nat_repr//task-clock: +97ms (+8.00%)
• 🟥 compiled/nat_repr//wall-clock: +98ms (+8.04%)
• ✅ elab/bv_decide_mul//maxrss: -13MiB (-1.82%)
• ✅ elab/bv_normalize_cast//maxrss: -13MiB (-2.67%)
• ✅ elab/cbv_leroy//maxrss: -131MiB (-6.93%)
• ✅ elab/cbv_system_f//maxrss: -84MiB (-3.70%)
• 🟥 elab/delayed_sharing//wall-clock: +23ms (+7.80%)
• ✅ elab/list_literal_nat//maxrss: -100MiB (-2.63%)
• 🟥 elab/list_literal_nat//wall-clock: +91ms (+4.20%)
• ✅ elab/simp_arith1//maxrss: -19MiB (-2.97%)
• ✅ elab/sym_arith_char//maxrss: -10MiB (-2.70%)
• ✅ interpreted/iterators//maxrss: -16MiB (-3.37%)
• ✅ lake/inundation/build/clean//maxrss: -25MiB (-2.85%)
• ✅ lake/inundation/config/elab//maxrss: -21MiB (-2.50%)
• ✅ lake/inundation/config/import//maxrss: -21MiB (-2.70%)
• ✅ lake/inundation/config/tree//maxrss: -22MiB (-2.71%)
• ✅ lake/inundation/env//maxrss: -22MiB (-2.74%)
• ✅ lake/inundation/setups//maxrss: -20MiB (-2.41%)
• ✅ misc/re-elab watchdog Init.Data.List.Sublist//maxrss: -20MiB (-3.40%)
• and 6 hidden