New linter source attribution helpers (67526ae)
Lean.Linter.Util now exposes findMatchingDecl?, findCodeQualitySource?, and findCodeQualitySource so linters can map syntax back to the declaration it belongs to. This improves code-quality diagnostics by letting them attribute issues to the right declaration instead of falling back blindly to the module.
Core elaboration context gets a cold subobject (
caeb31a)
More rarely-updated Core.Context fields were moved into Context.Cold, reducing reference-count traffic on hot elaboration paths like recursion-depth updates and withRef. The PR reports a measurable speedup in elaboration-heavy workloads, so this is a meaningful runtime optimization.
Missing Decidable for bif expressions (
3dfca7a)
Lean now has a Decidable (bif c then t else e) instance, analogous to the existing if/ite support. This fills a gap in the core API and makes conditional propositions work more smoothly in elaboration and proof automation.
Parser registers previously missing builtin node kinds (
9de8600)
Three builtin node kinds — fieldIdxKind, hexnumKind, and interpolatedStrKind — are now registered in Parser.Extension. This closes a parser infrastructure gap for syntax nodes that were already part of the language machinery.
