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.isDeprecatedSyntax (env : Environment) (kind : SyntaxNodeKind) : Bool

Whether kind is marked by deprecated_syntax.

Equations

• Lean.Elab.isDeprecatedSyntax env kind = (Lean.Elab.deprecatedSyntaxExt.getState env).contains kind

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 stx was written by the user (its head token has .original source info), the warning is attributed to the syntax itself even inside a macro expansion: enclosing macros (e.g. the internal namespace expansion of def Foo.bar ...) merely passed the user's syntax through. Only macro-generated syntax (synthetic source info, as produced by syntax quotations) is attributed to the macro call site via macroStack.

Equations

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