Skip to content

feat: add hint to unusedVariables linter#14259

Open
wkrozowski wants to merge 2 commits into
leanprover:masterfrom
wkrozowski:wojciech/unusedVariablesHint
Open

feat: add hint to unusedVariables linter#14259
wkrozowski wants to merge 2 commits into
leanprover:masterfrom
wkrozowski:wojciech/unusedVariablesHint

chore: render the hint with `[apply]` next to it

629bcd9
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
check-awaiting-manual
succeeded Jul 8, 2026 in 5s