f459c1436e
This PR upstreams `unusedDecidableInType` linter from mathlib. Stacked on top of #11313. --------- Co-authored-by: thorimur <thomasmurrills@gmail.com> Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
74 lines
3 KiB
Text
74 lines
3 KiB
Text
module
|
||
|
||
/-! # Tests for the `unusedDecidableInType` linter.
|
||
|
||
These exercise `linter.extra.unusedDecidableInType`, which warns when a theorem's hypotheses
|
||
include `Decidable*` instances that are not used in the remainder of the type. -/
|
||
|
||
set_option linter.extra.unusedDecidableInType true
|
||
|
||
variable (α : Type)
|
||
|
||
-- A theorem that doesn't use a `[DecidableEq α]` hypothesis at all.
|
||
/--
|
||
warning: `unusedEq` does not use the following hypothesis in its type:
|
||
• [DecidableEq α] (#2)
|
||
|
||
Consider removing this hypothesis and using `classical` in the proof instead. For terms, consider using `open scoped Classical in` at the term level (not the command level).
|
||
|
||
Note: This linter can be disabled with `set_option linter.extra.unusedDecidableInType false`
|
||
-/
|
||
#guard_msgs in
|
||
theorem unusedEq [DecidableEq α] : True := trivial
|
||
|
||
-- A theorem that doesn't use a `[Decidable p]` hypothesis at all.
|
||
/--
|
||
warning: `unusedDecidable` does not use the following hypothesis in its type:
|
||
• [Decidable p] (#2)
|
||
|
||
Consider removing this hypothesis and using `classical` in the proof instead. For terms, consider using `open scoped Classical in` at the term level (not the command level).
|
||
|
||
Note: This linter can be disabled with `set_option linter.extra.unusedDecidableInType false`
|
||
-/
|
||
#guard_msgs in
|
||
theorem unusedDecidable (p : Prop) [Decidable p] : True := trivial
|
||
|
||
-- Multiple unused `Decidable*` hypotheses are reported together.
|
||
/--
|
||
warning: `unusedMulti` does not use the following hypotheses in its type:
|
||
• [DecidableRel r] (#4)
|
||
• [DecidablePred q] (#5)
|
||
|
||
Consider removing these hypotheses and using `classical` in the proof instead. For terms, consider using `open scoped Classical in` at the term level (not the command level).
|
||
|
||
Note: This linter can be disabled with `set_option linter.extra.unusedDecidableInType false`
|
||
-/
|
||
#guard_msgs in
|
||
theorem unusedMulti (r : α → α → Prop) (q : α → Prop) [DecidableRel r] [DecidablePred q] :
|
||
True := trivial
|
||
|
||
-- The `[DecidableEq α]` hypothesis is used in the type, so no warning.
|
||
#guard_msgs in
|
||
theorem usedEq [DecidableEq α] (a b : α) : decide (a = b) = decide (a = b) := rfl
|
||
|
||
-- The `[Decidable p]` hypothesis is used only in the proof body, so the linter still warns.
|
||
/--
|
||
warning: `usedOnlyInProof` does not use the following hypothesis in its type:
|
||
• [Decidable p] (#2)
|
||
|
||
Consider removing this hypothesis and using `classical` in the proof instead. For terms, consider using `open scoped Classical in` at the term level (not the command level).
|
||
|
||
Note: This linter can be disabled with `set_option linter.extra.unusedDecidableInType false`
|
||
-/
|
||
#guard_msgs in
|
||
theorem usedOnlyInProof (p : Prop) [Decidable p] : True := by
|
||
if _ : p then trivial else trivial
|
||
|
||
-- Theorems in the `Decidable` namespace are exempt.
|
||
#guard_msgs in
|
||
theorem Decidable.exemptByNamespace [DecidableEq α] : True := trivial
|
||
|
||
-- Disabling the linter silences the warning.
|
||
#guard_msgs in
|
||
set_option linter.extra.unusedDecidableInType false in
|
||
theorem silenced [DecidableEq α] : True := trivial
|