Commit 2025-01-20 18:16 ec0f40db

feat: notation3-defined pretty printers now make tokens that are clickable in documentation (#20861) Modifies the notation3 delaborator generator so that when pp.tagAppFns is true, and when the expression being delaborated is the application of a constant, all the tokens of the notation are annotated with that constant. The consequence is that in docgen documentation, the tokens will be links to that constant. This heuristic might give unexpected results. For example, in

notation3 "Nat≥0" => { x : Nat // 0 ≤ x }

the documentation will have appearances of Nat≥0 link to Subtype. In complicated notations this heuristic may have mixed results. For example, it's possible to use notation3 to define notations that have different head constants in different expansions, and so the tokens can link to different constants in different appearances. There are no such cases of this in mathlib however. Zulip discussion