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

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

structure Lean.Linter.DeprecationEntry : Type

• newName? : Option Name
• text? : Option String
• since? : Option String

@[instance_reducible]

instance Lean.Linter.instInhabitedDeprecationEntry : Inhabited DeprecationEntry

Equations

• Lean.Linter.instInhabitedDeprecationEntry = { default := Lean.Linter.instInhabitedDeprecationEntry.default }

def Lean.Linter.mkSinceHint (stx : Syntax) : CoreM MessageData

Creates a hint for a missing (since := "...") clause that offers to append one with the current date to the deprecation syntax stx. Returns the empty message if stx has no source position.

Equations

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

opaque Lean.Linter.deprecatedAttr : ParametricAttribute DeprecationEntry

def Lean.Linter.setDeprecated {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (entry : DeprecationEntry) : m Unit

Equations

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

def Lean.Linter.isDeprecated (env : Environment) (declName : Name) : Bool

Equations

• Lean.Linter.isDeprecated env declName = (Lean.Linter.deprecatedAttr.getParam? env declName).isSome

def Lean.MessageData.isDeprecationWarning (msg : MessageData) : Bool

Equations

• msg.isDeprecationWarning = Lean.MessageData.hasTag (fun (x : Lean.Name) => x == `Lean.Linter.deprecatedAttr) msg

def Lean.Linter.getDeprecatedNewName (env : Environment) (declName : Name) : Option Name

Equations

• Lean.Linter.getDeprecatedNewName env declName = do let __do_lift ← Lean.Linter.deprecatedAttr.getParam? env declName __do_lift.newName?

def Lean.Linter.checkDeprecated (declName : Name) (allowSuggestion : Bool) : MetaM Unit

Equations

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