Unnecessary simpa code action

Stream: general

[Bhavik Mehta]

Can the unnecessary simpa linter be accompanied by a code action?

[Ruben Van de Velde]

Speaking of, didn't we have a code action for deprecated lemmas or is that just broken for me?

[Yaël Dillies]

We have two code snippets deprecated and deprecated alias (I encourage people to use them more!), and I believe @Damiano Testa wrote a deprecate to code action

[Damiano Testa]

I had an update_deprecation prototype, but it was round about the time when it looked like refactor would get merged, so I left it hanging.

[Damiano Testa]

I can look into it again, if there is a desire for it.

[Ruben Van de Velde]

No, I meant when using the deprecated lemma

[Eric Wieser]

This feels like it should be part of core

[Eric Wieser]

If core says "did you mean foo" when you write bar, it should be providing an action to replace bar with foo at the same time.