chore: clean up implementation of batteriesLinterExt

JovanGerb · JovanGerb · commit 26256a187f88 · 2026-02-08T13:51:36.000Z
diff --git a/Batteries/Tactic/Lint/Basic.lean b/Batteries/Tactic/Lint/Basic.lean
@@ -87,7 +87,7 @@ initialize batteriesLinterExt :
   registerSimplePersistentEnvExtension {
     addImportedFn := fun nss =>
       nss.foldl (init := {}) fun m ns => ns.foldl (init := m) addEntryFn
-    addEntryFn := fun m (n, b) => m.insert (n.updatePrefix .anonymous) (n, b)
+    addEntryFn
   }
 
 /--

Original file line number	Diff line number	Diff line change
`@@ -87,7 +87,7 @@ initialize batteriesLinterExt :`
`87`	`87`	`registerSimplePersistentEnvExtension {`
`88`	`88`	`addImportedFn := fun nss =>`
`89`	`89`	`nss.foldl (init := {}) fun m ns => ns.foldl (init := m) addEntryFn`
`90`		`- addEntryFn := fun m (n, b) => m.insert (n.updatePrefix .anonymous) (n, b)`
	`90`	`+ addEntryFn`
`91`	`91`	`}`
`92`	`92`
`93`	`93`	`/--`