dollarSyntaxLinter

Mathlib.Tactic.Linter.Style

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.Style.dollarSyntax.dollarSyntaxLinter

Lean4

@[inherit_doc linter.style.dollarSyntax]
def dollarSyntaxLinter : Linter where
  run :=
    withSetOptionIn fun stx ↦ do
      unless getLinterValue linter.style.dollarSyntax (← getLinterOptions) do
        return
      if (← MonadState.get).messages.hasErrors then
        return
      for s in findDollarSyntax stx do
        Linter.logLint linter.style.dollarSyntax s m!"Please use '<|' instead of '$' for the pipe operator."

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru