Topic: documenting notation
Johan Commelin (May 01 2020 at 18:51):
#2581 is the start of a PR that should document how to setup notation in Lean. That made me wonder: can we generate an overview of all notation currently introduced in mathlib? Could we add this to our docs pages? @Rob Lewis @Gabriel Ebner @Bryan Gin-ge Chen
Rob Lewis (May 01 2020 at 20:34):
I was going to answer "no, not without changes to core." Then I realized there's a very hackish way we could sort of do it now, reverse engineering the trick Gabriel added to linkify notation in the docs. But I think the hackish output won't be good enough.
Rob Lewis (May 01 2020 at 20:35):
That is, if we want to do it automatically, we need to change core. If someone wants to write things by hand, of course we can.
Last updated: May 14 2021 at 13:24 UTC