← Mathematical handbook

structure Lean.DeprecatedModuleEntry : Type

• message? : Option String
• since? : Option String

@[instance_reducible]

instance Lean.instInhabitedDeprecatedModuleEntry : Inhabited DeprecatedModuleEntry

Equations

• Lean.instInhabitedDeprecatedModuleEntry = { default := Lean.instInhabitedDeprecatedModuleEntry.default }

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

opaque Lean.deprecatedModuleExt : ModuleEnvExtension (Option DeprecatedModuleEntry)

def Lean.Environment.getDeprecatedModuleByIdx? (env : Environment) (idx : ModuleIdx) : Option DeprecatedModuleEntry

Equations

• env.getDeprecatedModuleByIdx? idx = (Lean.deprecatedModuleExt.getStateByIdx? env idx).join

def Lean.Environment.setDeprecatedModule (entry : Option DeprecatedModuleEntry) (env : Environment) : Environment

Equations

• Lean.Environment.setDeprecatedModule entry env = Lean.PersistentEnvExtension.setState Lean.deprecatedModuleExt env entry

def Lean.formatDeprecatedModuleWarning (env : Environment) (idx : ModuleIdx) (modName : Name) (entry : DeprecatedModuleEntry) : String

Equations

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