haveLetLinter

Mathlib.Tactic.Linter.HaveLetLinter

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.haveLet.haveLetLinter

Lean4

/-- The main implementation of the `have` vs `let` linter. -/
def haveLetLinter : Linter where
  run :=
    withSetOptionIn fun _stx => do
      let gh := linter.haveLet.get (← getOptions)
      unless gh != 0 && (← getInfoState).enabled do
        return
      unless gh == 1 && (← MonadState.get).messages.unreported.isEmpty do
        let trees ← getInfoTrees
        for t in trees do
          for (s, fmt) in ← nonPropHaves t do
            logLint0Disable linter.haveLet s
                m! "'{fmt}' is a Type and not a Prop. Consider using 'let' instead of 'have'."

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

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

Разделы

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

Аффилиация

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