Commit 2025-04-05 12:10 bdc275fd
View on Github →refactor: protect "map_add" lemmas (#23451)
Protect some lemmas in non-root namespaces called map_add
or similar, and remove lots of explicit _root_
prefixes (about 80 of them, at a cost of only 8 places where an explicit non-root prefix needed to be added.)