adaptationNoteLinter

Mathlib.Tactic.Linter.TextBased

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.TextBased.adaptationNoteLinter

Lean4

@[inherit_doc linter.adaptationNote]
def adaptationNoteLinter : TextbasedLinter := fun opts lines ↦
  Id.run
    (do
      unless getLinterValue linter.adaptationNote opts do
        return (#[], none)
      let mut errors := Array.mkEmpty 0
      for h : idx in [:lines.size]do
        -- We make this shorter to catch "Adaptation note", "adaptation note" and a missing colon.

        if lines[idx].containsSubstr "daptation note" then
          errors := errors.push (StyleError.adaptationNote, idx + 1)
      return (errors, none))

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

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

Разделы

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

Аффилиация

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