Commit 2024-08-19 07:41 5f6e1ba9
View on Github →feat: the dollarSyntax linter (#15909)
Lint against being $ used in place of the canonical <|: this is documented in the mathlib style guide.
feat: the dollarSyntax linter (#15909)
Lint against being $ used in place of the canonical <|: this is documented in the mathlib style guide.