PR #11606: feat(tactic/lint): adding a new linter for iff's

Stream: triage

[Random Issue Bot]

Today I chose PR 11606 for discussion!

feat(tactic/lint): adding a new linter for iff's
Created by @Arthur Paulino (@arthurpaulino) on 2022-01-22
Labels: meta, merge-conflict, linter

Is this PR still relevant? Any recent updates? Anyone making progress?

[Arthur Paulino]

Is everyone okay If I close this one?

If we don't want this linter, we might as well close #1924

[Arthur Paulino]

Full context of the PR is here

[Arthur Paulino]

Also pinging @Rob Lewis because he was the one who opened #1924

[Rob Lewis]

I think the linters are best when the fraction of nolints will be very small, and there are plenty of situations where we break the "implicit args to iff lemmas" customs, including the ones @Yaël Dillies points out. So I'm not sure we want this linter to be enforced in CI. But it's still a useful check and I'd be happy to have it as an opt-in linter, if you're interested in updating it?

[Rob Lewis]

Basically, just don't tag it with @[linter].

[Arthur Paulino]

@Rob Lewis do you want me to make it flag equalities too?

[Rob Lewis]

I think there are even more exceptions for equalities than for iffs, so probably not?

[Arthur Paulino]

Okay, the PR is ready :+1:

[Yaël Dillies]

Can you please give a more pertinent title (of course you're adding a linter if it's feat) and show the precise file?

[Arthur Paulino]

@Yaël Dillies I changed the PR title. And what do you mean by "precise file"? The PR only changes one file

[Yaël Dillies]

and it's not tactic/lint.lean

[Arthur Paulino]

Ah, you mean in the PR title as well. done