This PR fixes `processDefDeriving` to propagate the `meta` attribute to
instances derived via delta deriving, so that `deriving BEq` inside a
`public meta section` produces a meta instance. Previously the derived
`instBEqFoo` was not marked meta, and the LCNF visibility checker
rejected meta definitions that used `==` on the alias — this came up
while bumping verso to v4.30.0-rc1.
`processDefDeriving` now computes `isMeta` from two sources:
1. `(← read).isMetaSection` — true inside a `public meta section`,
covering the original issue #13313.
2. `isMarkedMeta (← getEnv) declName` — true when the type being derived
for was individually marked `meta` (e.g. `meta def Foo := Nat`), via
`elabMutualDef` in `src/Lean/Elab/MutualDef.lean`.
This value is passed to `wrapInstance` for aux declarations and to the
new `addAndCompile (markMeta := ...)` parameter from #13311, matching
how the regular command elaboration pipeline handles meta definitions.
Existing regression tests `tests/elab/13043.lean` and
`tests/elab/12897.lean` already cover meta-section + `wrapInstance` aux
def interaction. The new `tests/elab/13313.lean` specifically covers the
delta-derived `BEq` + LCNF-use case (the original issue) and an explicit
`meta def ... deriving BEq` outside a meta section (motivating the
second disjunct).
- [ ] depends on: #13311Closes#13313🤖 Prepared with Claude Code
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
