Lean4
/-- `unlintedNodes` contains the `SyntaxNodeKind`s for which there is no clear formatting preference:
if they appear in surface syntax, the linter will ignore formatting.
Currently, the unlined nodes are mostly related to `Subtype`, `Set` and `Finset` notation and
list notation.
-/
abbrev unlintedNodes :=
#[
-- # set-like notations, have extra spaces around the braces `{` `}`
-- subtype, the pretty-printer prefers `{ a // b }`
``«term{_:_//_}»,
-- set notation, the pretty-printer prefers `{ a | b }`
`«term{_}»,
-- empty set, the pretty-printer prefers `{ }`
``«term{}»,
-- set builder notation, the pretty-printer prefers `{ a : X | p a }`
`Mathlib.Meta.setBuilder,
-- # misc exceptions
-- We ignore literal strings.
`str,
-- list notation, the pretty-printer prefers `a :: b`
``«term_::_»,
-- negation, the pretty-printer prefers `¬a`
``«term¬_»,
-- declaration name, avoids dealing with guillemets pairs `«»`
``Parser.Command.declId, `Mathlib.Tactic.superscriptTerm, `Mathlib.Tactic.subscript,
-- notation for `Bundle.TotalSpace.proj`, the total space of a bundle
-- the pretty-printer prefers `π FE` over `π F E` (which we want)
`Bundle.termπ__,
-- notation for `Finset.slice`, the pretty-printer prefers `𝒜 #r` over `𝒜 # r` (mathlib style)
`Finset.«term_#_»,
-- The docString linter already takes care of formatting doc-strings.
``Parser.Command.docComment,
-- The pretty-printer adds a space between the backticks and the actual name.
``Parser.Term.doubleQuotedName, ]
