mathematics_in_lean_source icon indicating copy to clipboard operation
mathematics_in_lean_source copied to clipboard

Published 20 hours ago • verified publisher icon avigad

Unused variables

Open avigad opened this issue 1 year ago • 0 comments

The linter currently complains about unused variables e.g. in fun a b aleb ↦ mf (mg aleb). We should probably explain this somewhere and then replace unused variables by underscores.

avigad avatar Jul 07 '23 18:07 avigad