Commit 2024-08-26 12:01 f1ae38aa
View on Github →feat: the lambdaSyntax linter (#15896) The mathlib style guide states clearly that using \lambda for anonymous functions is disallowed, and the fun keyword is preferred. This linter enforces this.
feat: the lambdaSyntax linter (#15896) The mathlib style guide states clearly that using \lambda for anonymous functions is disallowed, and the fun keyword is preferred. This linter enforces this.