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.

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

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

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

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

          Equations
            Instances For