chore: clean up implementation of batteriesLinterExt (#1661)

JovanGerb · fgdorais · web-flow · commit 3bdaf1ad9459 · 2026-02-13T02:03:17.000Z
Co-authored-by: François G. Dorais &lt;fgdorais@gmail.com&gt;
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`	`/--`