deprecated lemma from rw?

Stream: mathlib4

[Bhavik Mehta]

Should we disallow deprecated lemmas from appearing in the output of rw? (or deprioritise them?) As a beginner-friendly tactic and searching tactic, it's slightly unfortunate for the suggestion to immediately throw a warning (this came up in lftcm)

[Bhavik Mehta]

(cc @Linus Sommer) This came up since rw? suggested docs4#List.count_cons'

[Mario Carneiro]

Hm, I notice some other issues as well:

• count_cons' is not displayed as @[deprecated] in doc-gen
• There is no target for the deprecation warning, nor a comment explaining what to do. Presumably the intended replacement is List.count_cons?

[Henrik Böving]

Is deprecated a lean built-in attribute? If so I can add it to the list of attributes that doc-gen knows about.

[Mario Carneiro]

yes

[Mario Carneiro]

it would be nice if we found some solution to user attributes though... I need to brush off AttrDelab again

[Henrik Böving]

implemented.