Documentation

Lean.DeprecatedModule

source
structure Lean.DeprecatedModuleEntry :
Type
Instances For
    source
    @[implicit_reducible]
    instance Lean.instInhabitedDeprecatedModuleEntry :
    Inhabited DeprecatedModuleEntry
    source
    opaque Lean.linter.deprecated.module :
    Lean.Option Bool
    source
    opaque Lean.deprecatedModuleExt :
    ModuleEnvExtension (Option DeprecatedModuleEntry)
    source
    def Lean.Environment.getDeprecatedModuleByIdx? (env : Environment) (idx : ModuleIdx) :
    Option DeprecatedModuleEntry
    Instances For
      source
      def Lean.Environment.setDeprecatedModule (entry : Option DeprecatedModuleEntry) (env : Environment) :
      Environment
      Instances For
        source
        def Lean.formatDeprecatedModuleWarning (env : Environment) (idx : ModuleIdx) (modName : Name) (entry : DeprecatedModuleEntry) :
        String
        Instances For