26ad4d6972
This PR extracts the functional (lambda) passed to `brecOn` in structural recursion into a named `_f` helper definition (e.g. `foo._f`), similar to how well-founded recursion uses `._unary`. This way the functional shows up with a helpful name in kernel diagnostics rather than as an anonymous lambda. The `_f` definition is added with `.abbrev` kernel reducibility hints and the `@[reducible]` elaborator attribute, so the kernel unfolds it eagerly after `brecOn` iota-reduces. For inductive predicates, the previous inline lambda behavior is kept. To ensure that parent definitions still get the correct reducibility height (since `getMaxHeight` ignores `.abbrev` definitions), each `_f`'s body height is registered via a new `defHeightOverrideExt` environment extension. `getMaxHeight` checks this extension for all definitions, making the height computation transparent to the extraction. This change improves code size (a bit). It may regress kernel reduction times, especially if a function defined by structural recursion is used in kernel reduction proofs on the hot path. Functions defined by structural recursion are not particularly fast to reduce anyways (due to the `.brecOn` construction), so already now it may be worth writing a kernel-reduction-friendly function manually (using the recursor directly, avoiding overloaded operations). This change will guide you in knowing which function to optimize. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
21 lines
588 B
Text
21 lines
588 B
Text
def fib (n : Nat) :=
|
|
match n with
|
|
| 0 | 1 => 1
|
|
| x+2 => fib x + fib (x+1)
|
|
termination_by structural n
|
|
|
|
/--
|
|
info: 573147844013817084101
|
|
---
|
|
trace: [diag] Diagnostics
|
|
[reduction] unfolded declarations (max: 400, num: 1):
|
|
[reduction] Nat.rec ↦ 400
|
|
[reduction] unfolded reducible declarations (max: 201, num: 2):
|
|
[reduction] Nat.casesOn ↦ 201
|
|
[reduction] fib._f ↦ 199
|
|
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
|
|
-/
|
|
#guard_msgs in
|
|
set_option diagnostics true in
|
|
set_option diagnostics.threshold 100 in
|
|
#reduce fib 100
|