chore: change UnusedSimpArgs hint#14313

wkrozowski merged 1 commit into

leanprover:masterleanprover/lean4:masterfrom

wkrozowski:wojciech/unusedSimpArgs-hintwkrozowski/lean4:wojciech/unusedSimpArgs-hintCopy head branch name to clipboard