linter.fugue.lambda

pp.unicode.fun is on project-wide, so anonymous functions are written λ x ↦ y. This linter flags the fun keyword — the inverse of Mathlib's linter.style.lambdaSyntax.