adding a prime to NameMapExtension

Author: kim-em

Mathlib/Tactic/Eqns.lean

@@ -37,7 +37,7 @@ open Lean Elab
 
 syntax (name := eqns) "eqns" (ppSpace ident)* : attr
 
-initialize eqnsAttribute : NameMapExtension (Array Name) ←
+initialize eqnsAttribute : NameMapExtension' (Array Name) ←
   registerNameMapAttribute {
     name  := `eqns
     descr := "Overrides the equation lemmas for a declaration to the provided list"

Mathlib/Tactic/Simps/Basic.lean

@@ -415,8 +415,8 @@ structure, used by the `@[simps]` attribute.
 - The first argument is the list of names of the universe variables used in the structure
 - The second argument is an array that consists of the projection data for each projection.
 -/
-initialize structureExt : NameMapExtension (List Name × Array ProjectionData) ←
-  registerNameMapExtension (List Name × Array ProjectionData)
+initialize structureExt : NameMapExtension' (List Name × Array ProjectionData) ←
+  registerNameMapExtension' (List Name × Array ProjectionData)
 
 /-- Projection data used internally in `getRawProjections`. -/
 structure ParsedProjectionData where

Mathlib/Tactic/Simps/NotationClass.lean

@@ -104,8 +104,8 @@ deriving Inhabited
 
 /-- `@[notation_class]` attribute. Note: this is *not* a `NameMapAttribute` because we key on the
 argument of the attribute, not the declaration name. -/
-initialize notationClassAttr : NameMapExtension AutomaticProjectionData ← do
-  let ext ← registerNameMapExtension AutomaticProjectionData
+initialize notationClassAttr : NameMapExtension' AutomaticProjectionData ← do
+  let ext ← registerNameMapExtension' AutomaticProjectionData
   registerBuiltinAttribute {
     name := `notation_class
     descr := "An attribute specifying that this is a notation class. Used by @[simps]."

Mathlib/Tactic/Translate/Core.lean

@@ -139,7 +139,7 @@ register_option linter.translateReorder : Bool := {
     equal to the automatically generated one" }
 
 @[inherit_doc translate_change_numeral]
-initialize changeNumeralAttr : NameMapExtension (List Nat) ←
+initialize changeNumeralAttr : NameMapExtension' (List Nat) ←
   registerNameMapAttribute {
     name := `translate_change_numeral
     descr :=
@@ -162,9 +162,9 @@ structure TranslateData : Type where
   involved when translating.
   This helps the translation heuristic by also transforming definitions if `ℕ` or another
   fixed type occurs as one of these arguments. -/
-  ignoreArgsAttr : NameMapExtension (List Nat)
+  ignoreArgsAttr : NameMapExtension' (List Nat)
   /-- `argInfoAttr` stores the declarations that need some extra information to be translated. -/
-  argInfoAttr : NameMapExtension ArgInfo
+  argInfoAttr : NameMapExtension' ArgInfo
   /-- The global `do_translate`/`dont_translate` attributes specify whether operations on
   a given type should be translated. `dont_translate` can be used for types that are translated,
   such as `MonoidAlgebra` -> `AddMonoidAlgebra`, or for fixed types, such as `Fin n`/`ZMod n`.
@@ -174,10 +174,10 @@ structure TranslateData : Type where
   Note: The name generation is not aware of `dont_translate`, so if some part of a lemma is not
     translated thanks to this, you generally have to specify the translated name manually.
   -/
-  doTranslateAttr : NameMapExtension Bool
+  doTranslateAttr : NameMapExtension' Bool
   /-- `translations` stores all of the constants that have been tagged with this attribute,
   and maps them to their translation. -/
-  translations : NameMapExtension Name
+  translations : NameMapExtension' Name
   /-- The name of the attribute, for example `to_additive` or `to_dual`. -/
   attrName : Name
   /-- If `changeNumeral := true`, then try to translate the number `1` to `0`. -/

Mathlib/Tactic/Translate/ToAdditive.lean

@@ -251,7 +251,7 @@ macro "to_additive?" rest:attrArgs : attr => `(attr| to_additive ? $rest)
 
 
 @[inherit_doc to_additive_ignore_args]
-initialize ignoreArgsAttr : NameMapExtension (List Nat) ←
+initialize ignoreArgsAttr : NameMapExtension' (List Nat) ←
   registerNameMapAttribute {
     name := `to_additive_ignore_args
     descr :=
@@ -263,10 +263,10 @@ initialize ignoreArgsAttr : NameMapExtension (List Nat) ←
         return ids.toList }
 
 @[inherit_doc TranslateData.argInfoAttr]
-initialize argInfoAttr : NameMapExtension ArgInfo ← registerNameMapExtension _
+initialize argInfoAttr : NameMapExtension' ArgInfo ← registerNameMapExtension' _
 
 @[inherit_doc TranslateData.doTranslateAttr]
-initialize doTranslateAttr : NameMapExtension Bool ← registerNameMapExtension _
+initialize doTranslateAttr : NameMapExtension' Bool ← registerNameMapExtension' _
 
 initialize
   registerBuiltinAttribute {
@@ -281,7 +281,7 @@ initialize
     add name _ _ := doTranslateAttr.add name false }
 
 /-- Maps multiplicative names to their additive counterparts. -/
-initialize translations : NameMapExtension Name ← registerNameMapExtension _
+initialize translations : NameMapExtension' Name ← registerNameMapExtension' _
 
 @[inherit_doc GuessName.GuessNameData.nameDict]
 def nameDict : Std.HashMap String (List String) := .ofList [

Mathlib/Tactic/Translate/ToDual.lean

@@ -89,7 +89,7 @@ syntax (name := to_dual) "to_dual" "?"? attrArgs : attr
 macro "to_dual?" rest:attrArgs : attr => `(attr| to_dual ? $rest)
 
 @[inherit_doc to_dual_ignore_args]
-initialize ignoreArgsAttr : NameMapExtension (List Nat) ←
+initialize ignoreArgsAttr : NameMapExtension' (List Nat) ←
   registerNameMapAttribute {
     name  := `to_dual_ignore_args
     descr :=
@@ -101,10 +101,10 @@ initialize ignoreArgsAttr : NameMapExtension (List Nat) ←
         return ids.toList }
 
 @[inherit_doc TranslateData.argInfoAttr]
-initialize argInfoAttr : NameMapExtension ArgInfo ← registerNameMapExtension _
+initialize argInfoAttr : NameMapExtension' ArgInfo ← registerNameMapExtension' _
 
 @[inherit_doc TranslateData.doTranslateAttr]
-initialize doTranslateAttr : NameMapExtension Bool ← registerNameMapExtension _
+initialize doTranslateAttr : NameMapExtension' Bool ← registerNameMapExtension' _
 
 initialize
   registerBuiltinAttribute {
@@ -119,7 +119,7 @@ initialize
     add name _ _ := doTranslateAttr.add name false }
 
 /-- Maps names to their dual counterparts. -/
-initialize translations : NameMapExtension Name ← registerNameMapExtension _
+initialize translations : NameMapExtension' Name ← registerNameMapExtension' _
 
 @[inherit_doc GuessName.GuessNameData.nameDict]
 def nameDict : Std.HashMap String (List String) := .ofList [