e0de32ad48
This PR switches `normalizeInstance` from using `isMetaSection` to the existing `declName?` pattern (already used by `unsafe` in `BuiltinNotation.lean` and `private_decl%` in `BuiltinTerm.lean`) for determining whether aux defs should be marked `meta`. #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: ``` Invalid definition `instInhabitedLibraryNote`, may not access declaration `instInhabitedLibraryNote._aux_1` marked as `meta` ``` The `declName?` pattern 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 `declName?.any (isMarkedMeta env)` is true and aux defs are correctly marked meta - **`deriving`**: `declName?` is `none` (the deriving handler runs outside `withDeclName`), so `isMeta` is `false` and aux defs are not marked meta — matching the instance itself, which the deriving handler also does not mark meta Found while adapting Batteries to nightly-2026-03-23. 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
20 lines
353 B
Text
20 lines
353 B
Text
-- Tests that `deriving` instances inside a `meta section` are properly marked `meta`.
|
|
-- Regression test for https://github.com/leanprover/lean4/pull/13043
|
|
|
|
module
|
|
|
|
public meta import Lean.Elab.Command
|
|
|
|
public meta section
|
|
|
|
namespace Test
|
|
|
|
open Lean
|
|
|
|
@[expose] def Foo := Unit
|
|
deriving Inhabited
|
|
|
|
@[expose] def Bar := Name
|
|
deriving Inhabited
|
|
|
|
end Test
|