Zulip Chat Archive

Stream: general

Topic: linkifiers

Kenny Lau (May 19 2020 at 08:08):

is there a list of all the linkifiers?

Rob Lewis (May 19 2020 at 08:09):

Can you see this page? https://leanprover.zulipchat.com/#organization/filter-settings

Rob Lewis (May 19 2020 at 08:09):

Not sure if it's only visible to admins.

Kenny Lau (May 19 2020 at 08:09):

yeah I can see it

Rob Lewis (May 21 2020 at 09:20):

Advertising this in general since not many people read the "Zulip meta" stream: docs#real.pi or src#real.pi will locate declarations for you.

Last updated: Dec 20 2023 at 11:08 UTC