Skip to content

Commit d14ff0b

Browse files
authored
chore: fix namespaceing in DeprecatedModule (#14310)
This PR fixes namespacing in `DeprecatedModule` to match the convention used throughout the codebase.
1 parent 81074d1 commit d14ff0b

1 file changed

Lines changed: 6 additions & 2 deletions

File tree

src/Lean/DeprecatedModule.lean

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,12 +25,16 @@ register_builtin_option linter.deprecated.module : Bool := {
2525
builtin_initialize deprecatedModuleExt : ModuleEnvExtension <| Option DeprecatedModuleEntry ←
2626
registerModuleEnvExtension <| pure none
2727

28-
def Environment.getDeprecatedModuleByIdx? (env : Environment) (idx : ModuleIdx) : Option DeprecatedModuleEntry :=
28+
namespace Environment
29+
30+
def getDeprecatedModuleByIdx? (env : Environment) (idx : ModuleIdx) : Option DeprecatedModuleEntry :=
2931
deprecatedModuleExt.getStateByIdx? env idx |>.join
3032

31-
def Environment.setDeprecatedModule (entry : Option DeprecatedModuleEntry) (env : Environment) : Environment :=
33+
def setDeprecatedModule (entry : Option DeprecatedModuleEntry) (env : Environment) : Environment :=
3234
deprecatedModuleExt.setState env entry
3335

36+
end Environment
37+
3438
def formatDeprecatedModuleWarning (env : Environment) (idx : ModuleIdx) (modName : Name)
3539
(entry : DeprecatedModuleEntry) : String :=
3640
let msg := entry.message?.getD ""

0 commit comments

Comments
 (0)