opaque Lean.Linter.Coe.linter.deprecatedCoercions : Lean.Option Bool

set_option linter.deprecatedCoercions true enables a linter emitting warnings on deprecated coercions.

def Lean.Linter.Coe.shouldWarnOnDeprecatedCoercions {m : Type → Type} [Monad m] [MonadOptions m] : m Bool

Checks whether the "deprecated coercions" linter is enabled.

Equations

• Lean.Linter.Coe.shouldWarnOnDeprecatedCoercions = do let __do_lift ← Lean.getOptions pure (Lean.KVMap.get __do_lift Lean.Linter.Coe.linter.deprecatedCoercions.name true)

def Lean.Linter.Coe.coercionsBannedInCore : Array Name

A list of coercion names that must not be used in core.

Equations

• Lean.Linter.Coe.coercionsBannedInCore = #[`optionCoe, `instCoeSubarrayArray]

def Lean.Linter.Coe.coeLinter : Linter

Validates that no coercions are used that are either deprecated or are banned in core.

Equations

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