Unused `Decidable*` instances linter: style?

Stream: mathlib4

[Thomas Murrills]

I'm currently porting the unused Decidable* instances linter, which checks if there's a Decidable* instance in a theorem's type and suggests removing it in favor of using classical in the proof instead. :)

I'd like to include a Try this: suggestion that removes the binder and also inserts classical in the body. This is easy enough if the body happens to be a by block, but what should the style be if the body is a term?

We could have an instance in before the term, but that seems bulky to me; we could open Classical somewhere, but a different linter seems to discourage this. We could also have a classical% (or classical;, like have ...;) term elaborator.

What's the best style option here? :)

[Damiano Testa]

Side question: how are you passing a Try this suggestion from a linter?

[Thomas Murrills]

Try this functionality now works in MessageData, since MessageData now supports widgets! :) (There’s still no lightbulb code action, but the suggestion is clickable in the infoview.)

[Damiano Testa]

That's great news!

[Eric Wieser]

open scoped Classical in term_proof?

[Aaron Liu]

by classical exact

[Eric Wieser]

That doesn't bind variables (unless I'm forgetting how that works)

[Aaron Liu]

what do you mean "bind variables"?

[Aaron Liu]

if you're talking about autolambda then I'm pretty sure exact does that

[Eric Wieser]

I'm talking about how def and theorem choose which variables to bind, but perhaps my complaint applies only to def

[Thomas Murrills]

Eric Wieser said:

open scoped Classical in term_proof?

Is this not the thing that other linter discourages? Or is it only discouraged at the command level or something?

[Eric Wieser]

Which linter?

[Aaron Liu]

it's discouraged to do it when it could affect the statement of your lemma

[Eric Wieser]

It's very discouraged without in, and somewhat discouraged at the command level for the reason that Aaron states

[Thomas Murrills]

I think it might be called the “open scoped classical” linter :grinning_face_with_smiling_eyes:

[Thomas Murrills]

(on mobile right now)

[Eric Wieser]

The term mode classical scope is not discouraged at all

[Thomas Murrills]

Ok, great! I think I might prefer open scoped to by classical exact just to avoid introducing any metavariable synthesis timing shenanigans.

[Thomas Murrills]

(Unless, of course, we ultimately want a term mode macro for open scoped Classical in for good style, which would be motivated by paralleling the tactic syntax and making source look a bit cleaner. Would obscure things a bit, but might be nice to have a uniform spelling across term and tactic mode.

But that would be a separate discussion which shouldn’t block this one, and the linter could just adapt if that becomes the style. :grinning_face_with_smiling_eyes:)