batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: make the unreachable tactic linter complain if tactics are called with no goals remaining

Open alexjbest opened this issue 2 years ago • 3 comments

alexjbest avatar Jul 12 '23 11:07 alexjbest

The unreachableTactic linter already has a whitelist for tactics that are supposed to be unreachable (like the unreachable tactic, or the body of the stop tactic). Things like tada and done would similarly be whitelisted from the noGoals linter.

digama0 avatar Jul 18 '23 16:07 digama0

@digama0 gave me some feedback on this in person in Leiden, which i'll try to address in the next few days: the main point was that this should be reimplemented as a separate linter (possibly using the same internals) so that users can more easily opt in or out of it, as it does serve a different purpose to the existing linter.

alexjbest avatar Jul 19 '23 16:07 alexjbest

Heartbeat check: is this PR still active? If it is then just give a thumbs up and I will delete this comment.

fgdorais avatar Jul 23 '24 10:07 fgdorais