Zulip Chat Archive

Stream: general

Topic: Where is #where?

Damiano Testa (Apr 30 2022 at 17:39):

Should #where appear somewhere in the online resources? For instance in the glossary page?

Kyle Miller (Apr 30 2022 at 17:44):

https://leanprover-community.github.io/mathlib_docs/commands.html##where

Damiano Testa (Apr 30 2022 at 17:46):

Oh, i had never seen this page, thanks Kyle!

Eric Wieser (Apr 30 2022 at 20:26):

We have a linkifier too:
command#where

Kyle Miller (Apr 30 2022 at 20:42):

command##where

Kyle Miller (Apr 30 2022 at 21:31):

The linkifier regexp is command#(?P<decl>[a-zA-Z0-9_.'-]*[a-zA-Z0-9_'-]). Maybe command#(?P<decl>[a-zA-Z0-9_.'-#]*[a-zA-Z0-9_'-]) would work?

Eric Wieser (Apr 30 2022 at 21:41):

I made a comment in #Zulip meta to that end

Scott Morrison (May 01 2022 at 02:34):

command##where

Last updated: Dec 20 2023 at 11:08 UTC