Lean.Linter.Deprecated

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

Instances For

source

@[instance_reducible]

instance Lean.Linter.instInhabitedDeprecationEntry :

Inhabited DeprecationEntry

source

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.

Instances For

source

opaque Lean.Linter.deprecatedAttr :

ParametricAttribute DeprecationEntry

source

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

m Unit

Instances For

source

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

Bool

Instances For

source

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

Bool

Instances For

source

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

Option Name

Instances For

source

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

MetaM Unit

Instances For