lambdaSyntaxLinter

Mathlib.Tactic.Linter.Style

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.Style.lambdaSyntax.lambdaSyntaxLinter

Lean4

@[inherit_doc linter.style.lambdaSyntax]
def lambdaSyntaxLinter : Linter where
  run :=
    withSetOptionIn fun stx ↦ do
      unless getLinterValue linter.style.lambdaSyntax (← getLinterOptions) do
        return
      if (← MonadState.get).messages.hasErrors then
        return
      for s in findLambdaSyntax stx do
        if let .atom _ "λ" := s[0] then
          Linter.logLint linter.style.lambdaSyntax s[0]
              m!"\
                        Please use 'fun' and not 'λ' to define anonymous functions.\n\
                        The 'λ' syntax is deprecated in mathlib4."

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

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

Разделы

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

Аффилиация

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