## Stream: general

### Topic: attribute documentation

#### Reid Barton (Aug 17 2020 at 13:53):

Would it be possible for attributes to be indexed by whatever handles the documentation search, so I can just use docs#norm_cast, for example?

#### Rob Lewis (Aug 17 2020 at 13:59):

Not really, since there can be name clashes, but attr#ext attr#norm_cast%20attributes

#### Rob Lewis (Aug 17 2020 at 14:00):

The doc entry for @[norm_cast] should be renamed anyway

(deleted)

#### Reid Barton (Aug 17 2020 at 14:10):

oh I didn't know attr#. But there's also the search box which could be more helpful.

#### Reid Barton (Aug 17 2020 at 14:10):

BTW, did you know we have a lemma called docs#ext?

#### Rob Lewis (Aug 17 2020 at 14:13):

attr# is new as of 13 minutes ago, but my point is docs# can't find both an attribute and a declaration name if they can overlap.

#### Rob Lewis (Aug 17 2020 at 14:14):

Johan Commelin said:

Yes, linkifiers with spaces don't work very well :/

#### Reid Barton (Aug 17 2020 at 14:16):

I would just ignore the possibility of overlap

#### Reid Barton (Aug 17 2020 at 14:16):

documentation search is pretty much a "do what I mean" domain

#### Rob Lewis (Aug 17 2020 at 14:18):

Are you talking about the search box on the web page or really the docs# here? The overlap isn't theoretical, see tactic#ring vs docs#ring or tactic#group vs docs#group etc.

#### Reid Barton (Aug 17 2020 at 14:19):

I don't know! Just make it better! :upside_down:

#### Reid Barton (Aug 17 2020 at 14:20):

Attribute overlap is more theoretical, right? As I recall you can actually get rather confusing behavior otherwise

#### Reid Barton (Aug 17 2020 at 14:21):

So specifically what triggered this was "ml norm_cast" in my search bar not doing anything useful

#### Rob Lewis (Aug 17 2020 at 14:21):

I mean, you just pointed out an example!

Reid Barton said:

BTW, did you know we have a lemma called docs#ext?

#### Rob Lewis (Aug 17 2020 at 14:21):

It feels really weird to make this work for attributes but not tactics though. Why should ml norm_cast send you to the attribute and not the tactic?

#### Kevin Buzzard (Aug 17 2020 at 14:21):

Reid is clearly just observing now that the problem is impossible to solve in some sense

#### Rob Lewis (Aug 17 2020 at 14:21):

ext is a declaration, a tactic, and an attribute, hah.

Last updated: May 15 2021 at 23:13 UTC