feat: forbid non-reserved identifiers via withForbidden

[sgraf812]

This PR makes withForbidden stop a term at a non-reserved word used as an identifier, not just at a registered token. A parser like withForbidden "invariant" termParser now ends the term when it reaches a bare invariant, while invariant remains usable as an identifier everywhere else.

identFn rejects an identifier whose text is in forbiddenTks, mirroring the forbidden-token check in mkTokenAndFixPos. The check is guarded by forbiddenTks.isEmpty, so the common identifier path is unchanged.
We considered putting a unified check in tokenFn or mkIdResult, but decided against that. The former would move the check outside the cache and regress some benchmarks by ~1%. The latter forces a flag on mkIdResult and identFnAux because nameLitAux and rawLitFn must not forbid any tokens.

[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 a104164801f9cdf71dc671801a01c74c1f3bf8ab --onto 79bec6d064d8672cb10864cad3d9fd054b6917ae. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-17 12:41:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a104164801f9cdf71dc671801a01c74c1f3bf8ab --onto 25ba8c3d3bcb1dded7ff5a6f3b6044b0a7970198. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-20 15:46:16)

[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 a104164801f9cdf71dc671801a01c74c1f3bf8ab --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force reference manual CI using the force-manual-ci label. (2026-07-17 12:41:41)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a104164801f9cdf71dc671801a01c74c1f3bf8ab --onto 49ff95727f98d43984726b26742d17a1ceea9dd5. You can force reference manual CI using the force-manual-ci label. (2026-07-20 15:46:18)

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 44667e1 against a104164 are in. No significant results found. @sgraf812

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

Small changes (1✅, 2🟥)

• 🟥 build/module/Lean.Parser.Basic//instructions: +60.7M (+0.79%)
• 🟥 compiled/parser//instructions: +11.5M (+0.03%)
• ✅ elab/bv_decide_mod//maxrss: -96MiB (-4.76%)

[Rob23oba]

Shouldn't this be something handled directly in mkIdResult? Also we should do this on the basis of the raw string, not the name, we don't want to forbid «invariant».

[sgraf812]

Thanks for the review. Yes, we should do it on the raw string; the new test case tests for that now. While doing the check in mkIdResult means we can have just one check, it also means that mkIdResult (and its caller identFnAux) needs to be passed a flag for whether or not the forbidden set should be tested (it shouldn't be tested when called from rawIdentFn and nameLitAux). It's simpler to just duplicate the test in identFn.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 648cffa against a104164 are in. No significant results found. @sgraf812

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

Small changes (1✅, 2🟥)

• 🟥 build/module/Lean.Parser.Basic//instructions: +53.1M (+0.69%)
• 🟥 compiled/parser//instructions: +14.1M (+0.04%)
• ✅ elab/delayed_sharing//wall-clock: -23ms (-6.12%)