Commit 2025-10-09 10:59 d554a187

refactor: make library notes a definition (#23767) Make library notes a definition of Unit type, whose doc-string is the note's content. As a consequence,

• doc-gen will display all library notes without any custom logic,
• library notes are shown upon hover (via the use of the doc-string),
• go to definition for library notes is easy Automate this using a macro, which also enforces that all library notes are inside the Mathlib.LibraryNote namespace. Temporarily, we use the library_note2 name; if/when the batteries version is changed, we can reclaim the original name. This PR does not address how to refer to library notes nicely (in a way that is shown in the documentation, checked for typos, with sufficient imports ensured etc.). That is left to a future PR. This is proposal 2a from this zulip discussion: #mathlib4 > library notes @ 💬