[fushanbobfan]

What was wrong

verso-literate attaches a doc comment to the largest syntax node that contains exactly one definition site. In @[to_additive foo /-- ... -/] def bar, that node is declModifiers, which holds foo's definition site and bar's doc comment, so bar's doc comment goes to foo (#979).

What this changes

Attribute instances are handled first, innermost first. An instance with one remaining definition site takes the doc comments inside it and claims that site, and the rest of the command is matched against the sites left over. This follows the idea of the commit linked in the issue and also covers nested attributes such as @[to_additive (attr := to_additive baz /-- ... -/) foo /-- ... -/].

The new fixture LitConfig.Core.AttrDefinedConstant is an attribute that defines a constant named in the attribute, since to_additive lives in Mathlib. It sits under Core because the keyboard test in test_accessibility.py allows ten Tab presses through the navbar, and the Core subtree is collapsed there.

How it was tested

I ran the run steps of ci.yml and the other pull request workflows on Debian with TeX Live 2026, Inkscape and Playwright. Results on this branch:

• lake build, lake lint, ./generate.sh, ./src/tests/run_serve_test.sh, linkchecker and the type checks pass
• lake test -- --test-options --verbose --wfail --junit=errata-report.xml --markdown=errata-summary.md -- --check-tex: 812 passed, 0 failed
• src/tests/run_literate_browser_tests.sh: 168 passed, 4 skipped; 6 passed
• browser-tests/errata-widget: 55 passed; search, ToC, redirect and KaTeX tests: 118 passed; browser-tests/verso-html: 72 passed, 4 skipped; browser-tests/package-manual: 27 passed

With only VersoLiterateMain.lean reverted, lake test -- --test-options --wfail fails the new test: The docstring "The docstring of the first declaration." is not associated with AttrDocstrings.first.

No-Changelog: bugfix

Fixes #979