chore: turn defLemma linter into Lean.Linter and rename it to defProp (#13803)

wkrozowski · web-flow · commit 4e59cdf84144 · 2026-05-28T10:28:47.000Z
This PR renames the `defLemma` linter to `defProp` and clarifies
its warning message.

The linter is also moved out of the `EnvLinter` framework into its own
file
`Lean.Linter.DefProp`, since it now processes elaboration info trees per
command.
The helper `getDeclsByBody` is exposed in `Lean.Linter.Util` for reuse.
diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean
@@ -9,6 +9,7 @@ prelude
 public import Lean.Linter.Util
 public import Lean.Linter.Builtin
 public import Lean.Linter.ConstructorAsVariable
+public import Lean.Linter.DefProp
 public import Lean.Linter.Deprecated
 public import Lean.Linter.DocsOnAlt
 public import Lean.Linter.UnusedVariables
diff --git a/src/Lean/Linter/DefProp.lean b/src/Lean/Linter/DefProp.lean
@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
+-/
+module
+
+prelude
+public import Lean.Linter.Basic
+public import Lean.Linter.Util
+
+public section
+
+namespace Lean.Linter
+open Elab Command Meta Term
+
+/--
+Enables the `defProp` linter, which warns when a `def` is used to introduce a
+declaration whose type is a `Prop`. Such a declaration should be written using
+`theorem` instead.
+-/
+register_builtin_option linter.defProp : Bool := {
+  defValue := false
+  descr := "enable the `defProp` linter, which warns when a `def` is used to introduce \
+    a declaration whose type is a `Prop`; such a declaration should be written using \
+    `theorem` instead."
+}
+
+namespace DefProp
+
+@[inherit_doc linter.defProp]
+def defPropLinter : Linter where run := withSetOptionIn fun _ => do
+  unless getLinterValue linter.defProp (← getLinterOptions) do
+    return
+  if (← get).messages.hasErrors then
+    return
+  let env ← getEnv
+  for t in ← getInfoTrees do
+    for declName in getDeclsByBody t do
+      let some info := env.find? declName | continue
+      unless info.isDefinition do continue
+      let isPropType ← liftTermElabM <| isProp info.type
+      if isPropType then
+        logLintIf linter.defProp (← getRef) m!"\
+          Definition `{.ofConstName declName}` is a proposition; use `theorem` instead of `def`"
+
+builtin_initialize addLinter defPropLinter
+
+end DefProp
+end Lean.Linter
diff --git a/src/Lean/Linter/EnvLinter/Builtin.lean b/src/Lean/Linter/EnvLinter/Builtin.lean
@@ -25,18 +25,6 @@ public meta section
 
 namespace Lean.Linter.EnvLinter
 
-/-- A linter for checking whether the correct declaration constructor (`def` or `theorem`)
-has been used. A `def` whose type is a `Prop` should be a `theorem`, and vice versa. -/
-@[builtin_env_linter] def defLemma : EnvLinter where
-  noErrorsFound := "All declarations correctly marked as def/lemma."
-  errorsFound := "INCORRECT DEF/LEMMA:"
-  test declName := do
-    if ← isAutoDecl declName then return none
-    let info ← getConstInfo declName
-    if info.isDefinition then
-      if ← isProp info.type then return some "is a def, should be a lemma/theorem"
-    return none
-
 /--
 `univParamsGrouped e nm₀` computes for each `Level` occurring in `e` the set of level parameters
 that appear in it, returning the collection of such parameter sets.
diff --git a/src/Lean/Linter/Extra/UnusedDecidableInType.lean b/src/Lean/Linter/Extra/UnusedDecidableInType.lean
@@ -15,6 +15,7 @@ public import Lean.Meta.ForEachExpr
 public import Lean.Meta.Sorry
 public import Lean.PrivateName
 public import Lean.Server.InfoUtils
+public import Lean.Linter.Util
 
 public section
 
@@ -253,18 +254,6 @@ private def onUnusedInstancesWhere (decl : ConstantVal) (p : Expr → Bool)
             }
           logOnUnused unusedParams
 
-/-- Get the `parentDecl`s of every elaborated body in the infotree. -/
-private def getDeclsByBody (t : InfoTree) : List Name :=
-  t.collectNodesBottomUp fun ctx i _ decls =>
-    match i with
-    | .ofCustomInfo i =>
-      if i.value.typeName == ``Lean.Elab.Term.BodyInfo then
-        if let some decl := ctx.parentDecl? then
-          decl :: decls
-        else decls
-      else decls
-    | _ => decls
-
 /--
 Get the declarations elaborated in the infotree `t` which are theorems according to the
 environment. This includes e.g. `instance`s of `Prop` classes in addition to declarations declared
diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean
@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Server.InfoUtils
 public import Lean.Linter.Init
+public import Lean.Elab.Term
 
 public section
 
@@ -44,3 +45,15 @@ where
         return some []
     else
       return none)
+
+/-- Get the `parentDecl`s of every elaborated body in the infotree. -/
+def getDeclsByBody (t : InfoTree) : List Name :=
+  t.collectNodesBottomUp fun ctx i _ decls =>
+    match i with
+    | .ofCustomInfo i =>
+      if i.value.typeName == ``Lean.Elab.Term.BodyInfo then
+        if let some decl := ctx.parentDecl? then
+          decl :: decls
+        else decls
+      else decls
+    | _ => decls
diff --git a/tests/elab/env_linter.lean b/tests/elab/env_linter.lean
@@ -131,7 +131,7 @@ def testGetChecksDefault : CoreM (Array Name) := do
   return checks.map (·.name)
 
 -- dummyBadName and checkUnivs are default, dummyExtraLinter is not
-/-- info: #[`checkUnivs, `defLemma, `dummyBadName] -/
+/-- info: #[`checkUnivs, `dummyBadName] -/
 #guard_msgs in
 #eval testGetChecksDefault
 
@@ -140,7 +140,7 @@ def testGetChecksExtra : CoreM (Array Name) := do
   let checks ← getChecks (scope := .extra) (runOnly := none)
   return checks.map (·.name)
 
-/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyExtraLinter] -/
+/-- info: #[`checkUnivs, `dummyBadName, `dummyExtraLinter] -/
 #guard_msgs in
 #eval testGetChecksExtra
 
@@ -149,7 +149,7 @@ def testGetChecksAll : CoreM (Array Name) := do
   let checks ← getChecks (scope := .all) (runOnly := none)
   return checks.map (·.name)
 
-/-- info: #[`checkUnivs, `defLemma, `dummyBadName, `dummyExtraLinter] -/
+/-- info: #[`checkUnivs, `dummyBadName, `dummyExtraLinter] -/
 #guard_msgs in
 #eval testGetChecksAll
 
@@ -181,7 +181,7 @@ def testLintCore : CoreM (Array (Name × Nat)) := do
   let results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters
   return results.map fun (linter, msgs) => (linter.name, msgs.size)
 
-/-- info: #[(`checkUnivs, 0), (`defLemma, 0), (`dummyBadName, 1)] -/
+/-- info: #[(`checkUnivs, 0), (`dummyBadName, 1)] -/
 #guard_msgs in
 #eval testLintCore
 
@@ -210,7 +210,7 @@ def testFormatResults : CoreM Format := do
   return (← msg.format)
 
 /--
-info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 3 linters
+info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 2 linters
 
 /- The `dummyBadName` linter reports:
 found bad names -/
@@ -229,7 +229,7 @@ def testFormatResultsClean : CoreM Format := do
   return (← msg.format)
 
 /--
-info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 3 linters
+info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 2 linters
 -/
 #guard_msgs in
 #eval testFormatResultsClean
diff --git a/tests/lake/tests/builtin-lint/ExtraViolations.lean b/tests/lake/tests/builtin-lint/ExtraViolations.lean
@@ -1,5 +1,9 @@
 import Linters
 
+-- `linter.defProp` is off by default for bootstrapping reasons; enable it
+-- here so `shouldBeTheoremUnderExtra` still fires when default linters run.
+set_option linter.defProp true
+
 -- This name ends with 'Extra' — the dummyExtra linter should flag it.
 def badNameExtra : Nat := 1
 
@@ -13,7 +17,7 @@ example : True := by
 -- the builtin extra `dupNamespace` text linter should flag it.
 def Dup.Dup.violation : Nat := 2
 
--- This uses `def` for a Prop — the default `defLemma` linter should flag this
+-- This uses `def` for a Prop — the default `defProp` linter should flag this
 -- whenever default linters run, including under `--extra`.
 def shouldBeTheoremUnderExtra : 1 = 1 := rfl
 
diff --git a/tests/lake/tests/builtin-lint/Main.lean b/tests/lake/tests/builtin-lint/Main.lean
@@ -1,14 +1,18 @@
 import Main.Sub
 
--- This uses `def` for a Prop — the `defLemma` linter should flag this.
+-- `linter.defProp` is off by default for bootstrapping reasons; enable it
+-- here so the test scenarios that exercise default lint mode still trigger it.
+set_option linter.defProp true
+
+-- This uses `def` for a Prop — the `defProp` linter should flag this.
 def shouldBeTheorem : 1 = 1 := rfl
 
--- This is annotated to be skipped by `defLemma` — no import needed.
-@[builtin_nolint defLemma]
+-- `set_option` disables `defProp` locally so this violation is not flagged.
+set_option linter.defProp false in
 def skippedViolation : 2 = 2 := rfl
 
 -- A `@[reducible, instance] def` of Prop type is still elaborated as a `def`,
--- so `defLemma` should flag it.
+-- so `defProp` should flag it.
 @[reducible, instance]
 def reducibleInstShouldBeTheorem : Nonempty Bool := ⟨true⟩
 
diff --git a/tests/lake/tests/builtin-lint/Main/Sub.lean b/tests/lake/tests/builtin-lint/Main/Sub.lean
@@ -1,5 +1,9 @@
--- Env-linter violation: `def` on a Prop — should be caught by `defLemma`
--- regardless of build-time options, since env linters run post-build.
+-- `linter.defProp` is off by default for bootstrapping reasons; enable it
+-- here so this transitive-import test still captures the violation in the
+-- module's lint log.
+set_option linter.defProp true
+
+-- `def` on a Prop — caught by the `defProp` linter at build time.
 def shouldBeTheoremInSub : 1 = 1 := rfl
 
 -- Default text-linter violation: `linter.unusedVariables` has `defValue := true`,
diff --git a/tests/lake/tests/builtin-lint/test.sh b/tests/lake/tests/builtin-lint/test.sh
@@ -30,10 +30,10 @@ lake_out lint --lint-only unusedVariables TextLints || true
 match_pat 'Variable name `unusedLet` is not explicitly referenced' produced.out
 no_match_pat 'missing doc string' produced.out
 
-# --builtin-lint should detect the defLemma violation in Main (the default target)
+# --builtin-lint should detect the defProp violation in Main (the default target)
 lake_out lint --builtin-lint || true
 match_pat 'shouldBeTheorem' produced.out
-match_pat 'is a def, should be a lemma/theorem' produced.out
+match_pat 'is a proposition; use `theorem` instead of `def`' produced.out
 # `@[reducible, instance]` on a `def` of Prop type keeps it a `def`, so flag it.
 match_pat 'reducibleInstShouldBeTheorem' produced.out
 # Plain `instance` of Prop type is elaborated as a theorem; it should not be flagged.
@@ -45,8 +45,8 @@ match_pat 'only occur together' produced.out
 # builtin_nolint checkUnivs should suppress the warning
 no_match_pat 'badUnivSkipped' produced.out
 
-# --lint-only defLemma should run only the defLemma linter
-lake_out lint --lint-only defLemma || true
+# --lint-only defProp should run only the defProp linter
+lake_out lint --lint-only defProp || true
 match_pat 'shouldBeTheorem' produced.out
 no_match_pat 'badUnivDecl' produced.out
 
@@ -57,8 +57,9 @@ no_match_pat 'badUnivDecl' produced.out
 # package, so passing any module of a package flips the flag for every module
 # in that package.
 
-# Env linters run post-build against `importModules`-loaded decls, so
-# `defLemma` catches `shouldBeTheoremInSub` regardless of override scope.
+# `defProp` runs during the build of each module, so its warning for
+# `shouldBeTheoremInSub` is captured in `Main.Sub`'s lint log and re-emitted
+# via `collectTextLints` when `Main` is linted.
 lake_out lint --builtin-lint Main || true
 match_pat 'shouldBeTheoremInSub' produced.out
 
@@ -81,7 +82,7 @@ test_run lint --builtin-only Clean
 
 # Without --extra, the extra linters (both the env linter and the dummy extra
 # text linter in Linters.lean) must not run. Default linters still do, so the
-# `defLemma` violation in this file fires.
+# default `defProp` linter's violation in this file fires.
 lake_out lint --builtin-only ExtraViolations || true
 no_match_pat 'badNameExtra' produced.out
 no_match_pat 'extra text linter saw a declaration' produced.out
@@ -91,7 +92,7 @@ no_match_pat 'tac1 <;> tac2' produced.out
 no_match_pat 'Dup.Dup.violation' produced.out
 # Builtin extra text linter `unreachableTactic` is non-default, so silent.
 no_match_pat 'this tactic is never executed' produced.out
-# Default env linter `defLemma` runs and flags the def-of-Prop in this file.
+# Default `defProp` linter runs and flags the def-of-Prop in this file.
 match_pat 'shouldBeTheoremUnderExtra' produced.out
 
 # --extra should run default linters together with the non-default (extra)
@@ -109,7 +110,7 @@ match_pat 'Dup.Dup.violation' produced.out
 match_pat "namespace .*Dup.* is duplicated" produced.out
 # Builtin `unreachableTactic` extra text linter fires under --extra.
 match_pat 'this tactic is never executed' produced.out
-# --extra also runs default linters, so `defLemma` flags this file's violation.
+# --extra also runs default linters, so `defProp` flags this file's violation.
 match_pat 'shouldBeTheoremUnderExtra' produced.out
 
 # --extra on TextLints: default `linter.unusedVariables` fires (default
@@ -141,15 +142,15 @@ no_match_pat 'badNameExtra' produced.out
 no_match_pat 'shouldBeTheorem' produced.out
 
 # Multiple --lint-only flags accumulate: both named linters should run
-lake_out lint --lint-only defLemma --lint-only checkUnivs || true
+lake_out lint --lint-only defProp --lint-only checkUnivs || true
 match_pat 'shouldBeTheorem' produced.out
 match_pat 'badUnivDecl' produced.out
 no_match_pat 'badNameExtra' produced.out
 
 # Last-wins: --extra overrides a prior --lint-all and clears --lint-only.
-# Since --extra runs both default and extra linters, the default `defLemma`
+# Since --extra runs both default and extra linters, the default `defProp`
 # violation in ExtraViolations.lean fires too.
-lake_out lint --lint-all --lint-only defLemma --extra || true
+lake_out lint --lint-all --lint-only defProp --extra || true
 match_pat 'badNameExtra' produced.out
 match_pat 'shouldBeTheoremUnderExtra' produced.out
 
@@ -160,13 +161,13 @@ match_pat 'badNameExtra' produced.out
 match_pat 'shouldBeTheorem' produced.out
 
 # Last-wins: --extra clears a previously accumulated --lint-only. Default
-# linters still run under --extra, so `defLemma` fires on its file's violation.
-lake_out lint --lint-only defLemma --extra || true
+# linters still run under --extra, so `defProp` fires on its file's violation.
+lake_out lint --lint-only defProp --extra || true
 match_pat 'badNameExtra' produced.out
 match_pat 'shouldBeTheoremUnderExtra' produced.out
 
 # --lint-only after --extra: the named linter runs (selection ignores scope)
-lake_out lint --extra --lint-only defLemma || true
+lake_out lint --extra --lint-only defProp || true
 match_pat 'shouldBeTheorem' produced.out
 no_match_pat 'badNameExtra' produced.out
 
@@ -193,7 +194,7 @@ lake_out lint --extra ExtraViolations || true
 match_pat 'badNameExtra' produced.out
 
 # --lint-only implicitly enables builtin lint
-lake_out lint --lint-only defLemma || true
+lake_out lint --lint-only defProp || true
 match_pat 'shouldBeTheorem' produced.out
 
 # builtinLint = false: check-lint fails (no lint driver and builtin linting disabled)
