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, and it does not affect rawIdent (field projections), the parenthesized escape via withoutForbidden, or reserved-token forbidding.

Preparatory for for … invariant … do do-notation and require/ensures contract clauses, whose clause keywords are deliberately non-reserved.

[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)

[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)

[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».