fix: use `declName?` pattern for `normalizeInstance` meta marking The previous fix (#13043) used `isMetaSection` to determine whether `normalizeInstance` aux defs should be marked `meta`. This caused `deriving` in meta sections to fail: the deriving handler doesn't mark the instance itself as meta, so the non-meta instance couldn't access its meta-marked aux defs. Switch to the existing `declName?` pattern (already used by `unsafe` and `private_decl%`), which inherits meta status from the parent declaration rather than the scope. This correctly handles both cases: - `inferInstanceAs`: parent declaration is marked meta by `processHeaders`, so aux defs are also marked meta - `deriving`: `declName?` reflects the actual meta status of the declaration being elaborated, avoiding the mismatch Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.