Documentation

Lean.Linter.Coe

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

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

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

Checks whether the "deprecated coercions" linter is enabled.

Instances For
    source
    def Lean.Linter.Coe.coercionsBannedInCore :
    Array Name

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

    Instances For
      source
      def Lean.Linter.Coe.coeLinter :
      Linter

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

      Instances For