cdotLinter — Mathlib

Lean4
@[inherit_doc linter.style.cdot]
def cdotLinter : Linter where
  run :=
    withSetOptionIn fun stx ↦ do
      unless getLinterValue linter.style.cdot (← getLinterOptions) do
        return
      if (← MonadState.get).messages.hasErrors then
        return
      for s in unwanted_cdot stx do
        Linter.logLint linter.style.cdot s m!"Please, use '·' (typed as `\\.`) instead of '.' as 'cdot'."
      for cdot in Mathlib.Linter.findCDot stx do
        match cdot.find? (·.isOfKind `token.«· ») with
        | some (.node _ _ #[.atom (.original _ _ afterCDot _) _]) =>
          if (afterCDot.takeWhile (·.isWhitespace)).contains '\n' then
            Linter.logLint linter.style.cdot cdot
                m!"This central dot `·` is isolated; please merge it with the next line."
        | _ =>
          return
Похожие утверждения