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

Commits

Commits on Aug 3, 2026

Commits on Aug 4, 2026

Commits on Aug 7, 2026