perf: link with identical code folding

[Kha]

No description provided.

[Kha]

!bench

[leanprover-radar]

Benchmark results for 1a8b9c3 against 4af9cc0 are in! @Kha

Runs (2🟥)

• 🟥 build exited with code 2
• 🟥 other exited with code 2

[Kha]

!bench

[leanprover-radar]

Benchmark results for a4030bc against 4af9cc0 are in! @Kha

Medium changes (1✅)

• ✅ nat_repr//instructions: -552.6M (-12.2%)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-01-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-16 10:56:07)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-16 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-01-16 10:56:09)
• ❌ Reference manual branch lean-pr-testing-12022 built against this PR, but generating HTML failed. (2026-01-25 17:31:34) View Log
• 🟡 Reference manual branch lean-pr-testing-12022 build against this PR didn't complete normally. (2026-01-25 17:33:16) View Log

[Kha]

!bench

[leanprover-radar]

Benchmark results for b2e8a8e against 4af9cc0 are in! @Kha

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• 🟥 build//instructions: +138.4M (+0.0%)

No significant changes detected.