opaque Lean.Linter.Extra.linter.extra.unusedDecidableInType : Lean.Option Bool

Enables the 'unused Decidable* in type' linter, which lints against Decidable* instance hypotheses in the types of theorems which are not used in the remainder of the type, and could therefore be replaced with classical in the proof.

This linter fires only on theorems. (This includes lemmas and instances of Prop classes.) The constants recognised as Decidable* are Decidable, DecidablePred, DecidableRel, DecidableEq, DecidableLE, and DecidableLT.

def Lean.Linter.Extra.UnusedDecidableInType.unusedDecidableInTypeLinter : Linter

Enables the 'unused Decidable* in type' linter, which lints against Decidable* instance hypotheses in the types of theorems which are not used in the remainder of the type, and could therefore be replaced with classical in the proof.

This linter fires only on theorems. (This includes lemmas and instances of Prop classes.) The constants recognised as Decidable* are Decidable, DecidablePred, DecidableRel, DecidableEq, DecidableLE, and DecidableLT.

Equations

• One or more equations did not get rendered due to their size.