Skip to content

[Merged by Bors] - feat(Tactic/Linter/UnusedTactic): also lint inside conv => - #42416

Closed
JovanGerb wants to merge 6 commits into
leanprover-community:masterfrom
JovanGerb:Jovan-unusedTactics-conv
Closed

[Merged by Bors] - feat(Tactic/Linter/UnusedTactic): also lint inside conv =>#42416
JovanGerb wants to merge 6 commits into
leanprover-community:masterfrom
JovanGerb:Jovan-unusedTactics-conv