opaque Lean.Linter.linter.deprecated.syntax : Lean.Option Bool

structure Lean.Elab.SyntaxDeprecationEntry : Type

Entry recording that a syntax kind has been deprecated.

• kind : SyntaxNodeKind

  The syntax node kind that is deprecated.

• text? : Option String

  Optional deprecation message.

• since? : Option String

  Optional version or date at which the syntax was deprecated.

opaque Lean.Elab.deprecatedSyntaxExt : SimplePersistentEnvExtension SyntaxDeprecationEntry (NameMap SyntaxDeprecationEntry)

def Lean.Elab.checkDeprecatedSyntax {m : Type → Type} [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m] [AddMessageContext m] [MonadRef m] (stx : Syntax) (macroStack : MacroStack) : m Unit

Check whether stx is a deprecated syntax kind, and if so, emit a warning.

If macroStack is non-empty, the warning is attributed to the macro call site rather than the syntax itself.

Equations

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