Skip to content

chore: change UnusedSimpArgs hint#14313

Merged
wkrozowski merged 1 commit into
leanprover:masterfrom
wkrozowski:wojciech/unusedSimpArgs-hint
Jul 8, 2026
Merged

chore: change UnusedSimpArgs hint#14313
wkrozowski merged 1 commit into
leanprover:masterfrom
wkrozowski:wojciech/unusedSimpArgs-hint

chore: change `UnusedSimpArgs` hint

dab05a2
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
check-pr-body
succeeded Jul 8, 2026 in 5s