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.

[Malvin Gattinger]

Sorry to revive this old topic, but I keep getting the deprecated docs#Eq.rec_eq_cast recommened by rw?. Did "implemented" here refer to a filter for rw? not to do this? Or only to making doc-gen know about it?

Example:

import Mathlib.Logic.Basic

example (h : A = B) (x : A) (y : B) : x = h ▸ y := by
  rw? -- Try this: rw [Eq.rec_eq_cast]
  sorry

example (h : A = B) (x : A) (y : B) : x = h ▸ y := by
  rw [Eq.rec_eq_cast] -- `Eq.rec_eq_cast` has been deprecated: Use `eqRec_eq_cast` instead
  sorry

example (h : A = B) (x : A) (y : B) : x = h ▸ y := by
  rw [eqRec_eq_cast]
  sorry

[Henrik Böving]

Making doc-gen know about the deprecation attribute