attribute documentation

Stream: general

[Reid Barton]

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]

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

[Rob Lewis]

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

[Johan Commelin]

That link is brok       en

[Gabriel Ebner]

(deleted)

[Reid Barton]

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

[Reid Barton]

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

[Rob Lewis]

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]

Johan Commelin said:

That link is brok       en

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

[Reid Barton]

I would just ignore the possibility of overlap

[Reid Barton]

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

[Rob Lewis]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Rob Lewis]

I mean, you just pointed out an example!

Reid Barton said:

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

[Rob Lewis]

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]

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

[Rob Lewis]

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