Zulip Chat Archive

Stream: general

Topic: documenting notation

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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