From eba400543d99be96ff7385d14314f4030a44d675 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 7 Jul 2022 13:41:04 +0200
Subject: [PATCH] refactor: use computed fields for Name

---
 src/Init/Meta.lean                            | 81 +++++++++++--------
 src/Init/Prelude.lean                         | 72 ++++++++---------
 src/Init/SizeOf.lean                          |  8 +-
 src/Lean/AuxRecursor.lean                     |  2 +-
 src/Lean/Compiler/ExportAttr.lean             |  6 +-
 src/Lean/Compiler/IR/Boxing.lean              |  5 +-
 src/Lean/Compiler/IR/EmitC.lean               | 12 +--
 src/Lean/Compiler/NameMangling.lean           |  4 +-
 src/Lean/Compiler/Util.lean                   |  8 +-
 src/Lean/Data/Name.lean                       | 78 +++++++++---------
 src/Lean/Data/NameTrie.lean                   |  4 +-
 src/Lean/Elab/Attributes.lean                 |  2 +-
 src/Lean/Elab/AutoBound.lean                  |  4 +-
 src/Lean/Elab/BuiltinCommand.lean             | 10 +--
 src/Lean/Elab/BuiltinNotation.lean            |  2 +-
 src/Lean/Elab/DeclModifiers.lean              |  4 +-
 src/Lean/Elab/DeclUtil.lean                   |  4 +-
 src/Lean/Elab/Declaration.lean                | 10 +--
 src/Lean/Elab/DefView.lean                    |  2 +-
 src/Lean/Elab/Deriving/Util.lean              |  4 +-
 src/Lean/Elab/Quotation.lean                  |  4 +-
 src/Lean/Elab/StructInst.lean                 |  4 +-
 src/Lean/Elab/Syntax.lean                     |  4 +-
 src/Lean/Elab/Term.lean                       |  2 +-
 src/Lean/Elab/Util.lean                       |  4 +-
 src/Lean/Environment.lean                     | 10 +--
 src/Lean/Hygiene.lean                         |  6 +-
 src/Lean/Message.lean                         |  2 +-
 src/Lean/Meta/RecursorInfo.lean               |  2 +-
 src/Lean/Meta/ReduceEval.lean                 |  4 +-
 src/Lean/Modifiers.lean                       | 14 ++--
 .../PrettyPrinter/Delaborator/Builtins.lean   | 12 +--
 src/Lean/ResolveName.lean                     | 10 +--
 src/Lean/Server/Completion.lean               | 10 +--
 src/Lean/Syntax.lean                          | 16 ++--
 src/Lean/Util/Path.lean                       |  4 +-
 src/Lean/Util/Trace.lean                      |  4 +-
 src/Lean/Widget/InteractiveDiagnostic.lean    |  2 +-
 src/lake                                      |  2 +-
 tests/lean/namelit.lean.expected.out          | 16 ++--
 tests/lean/run/998Export.lean                 |  6 +-
 tests/lean/run/printDecls.lean                |  2 +-
 42 files changed, 236 insertions(+), 226 deletions(-)

diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 2fbeb3fe35..b73abdae48 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -99,16 +99,16 @@ namespace Name
 
 def getRoot : Name → Name
   | anonymous             => anonymous
-  | n@(str anonymous _ _) => n
-  | n@(num anonymous _ _) => n
-  | str n _ _             => getRoot n
-  | num n _ _             => getRoot n
+  | n@(str anonymous _) => n
+  | n@(num anonymous _) => n
+  | str n _             => getRoot n
+  | num n _             => getRoot n
 
 @[export lean_is_inaccessible_user_name]
 def isInaccessibleUserName : Name → Bool
-  | Name.str _ s _   => s.contains '✝' || s == "_inaccessible"
-  | Name.num p _   _ => isInaccessibleUserName p
-  | _                => false
+  | Name.str _ s   => s.contains '✝' || s == "_inaccessible"
+  | Name.num p _   => isInaccessibleUserName p
+  | _              => false
 
 def escapePart (s : String) : Option String :=
   if s.length > 0 && isIdFirst (s.get 0) && (s.toSubstring.drop 1).all isIdRest then s
@@ -118,11 +118,11 @@ def escapePart (s : String) : Option String :=
 -- NOTE: does not roundtrip even with `escape = true` if name is anonymous or contains numeric part or `idEndEscape`
 variable (sep : String) (escape : Bool)
 def toStringWithSep : Name → String
-  | anonymous         => "[anonymous]"
-  | str anonymous s _ => maybeEscape s
-  | num anonymous v _ => toString v
-  | str n s _         => toStringWithSep n ++ sep ++ maybeEscape s
-  | num n v _         => toStringWithSep n ++ sep ++ Nat.repr v
+  | anonymous       => "[anonymous]"
+  | str anonymous s => maybeEscape s
+  | num anonymous v => toString v
+  | str n s         => toStringWithSep n ++ sep ++ maybeEscape s
+  | num n v         => toStringWithSep n ++ sep ++ Nat.repr v
 where
   maybeEscape s := if escape then escapePart s |>.getD s else s
 
@@ -131,7 +131,7 @@ protected def toString (n : Name) (escape := true) : String :=
   toStringWithSep "." (escape && !n.isInaccessibleUserName && !n.hasMacroScopes && !maybePseudoSyntax) n
 where
   maybePseudoSyntax :=
-    if let Name.str _ s _ := n.getRoot then
+    if let .str _ s := n.getRoot then
       -- could be pseudo-syntax for loose bvar or universe mvar, output as is
       "#".isPrefixOf s || "?".isPrefixOf s
     else
@@ -148,8 +148,8 @@ private def hasNum : Name → Bool
 protected def reprPrec (n : Name) (prec : Nat) : Std.Format :=
   match n with
   | anonymous => Std.Format.text "Lean.Name.anonymous"
-  | num p i _ => Repr.addAppParen ("Lean.Name.mkNum " ++ Name.reprPrec p max_prec ++ " " ++ repr i) prec
-  | str p s _ =>
+  | num p i => Repr.addAppParen ("Lean.Name.mkNum " ++ Name.reprPrec p max_prec ++ " " ++ repr i) prec
+  | str p s =>
     if p.hasNum then
       Repr.addAppParen ("Lean.Name.mkStr " ++ Name.reprPrec p max_prec ++ " " ++ repr s) prec
     else
@@ -161,23 +161,23 @@ instance : Repr Name where
 deriving instance Repr for Syntax
 
 def capitalize : Name → Name
-  | Name.str p s _ => Name.mkStr p s.capitalize
-  | n              => n
+  | .str p s => .str p s.capitalize
+  | n        => n
 
 def replacePrefix : Name → Name → Name → Name
-  | anonymous,     anonymous, newP => newP
-  | anonymous,     _,         _    => anonymous
-  | n@(str p s _), queryP,    newP => if n == queryP then newP else Name.mkStr (p.replacePrefix queryP newP) s
-  | n@(num p s _), queryP,    newP => if n == queryP then newP else Name.mkNum (p.replacePrefix queryP newP) s
+  | anonymous,   anonymous, newP => newP
+  | anonymous,   _,         _    => anonymous
+  | n@(str p s), queryP,    newP => if n == queryP then newP else Name.mkStr (p.replacePrefix queryP newP) s
+  | n@(num p s), queryP,    newP => if n == queryP then newP else Name.mkNum (p.replacePrefix queryP newP) s
 
 /--
   `eraseSuffix? n s` return `n'` if `n` is of the form `n == n' ++ s`.
 -/
 def eraseSuffix? : Name → Name → Option Name
-  | n,         anonymous   => some n
-  | str p s _, str p' s' _ => if s == s' then eraseSuffix? p p' else none
-  | num p s _, num p' s' _ => if s == s' then eraseSuffix? p p' else none
-  | _,         _           => none
+  | n,       anonymous => some n
+  | str p s, str p' s' => if s == s' then eraseSuffix? p p' else none
+  | num p s, num p' s' => if s == s' then eraseSuffix? p p' else none
+  | _,       _         => none
 
 /-- Remove macros scopes, apply `f`, and put them back -/
 @[inline] def modifyBase (n : Name) (f : Name → Name) : Name :=
@@ -190,21 +190,32 @@ def eraseSuffix? : Name → Name → Option Name
 @[export lean_name_append_after]
 def appendAfter (n : Name) (suffix : String) : Name :=
   n.modifyBase fun
-    | str p s _ => Name.mkStr p (s ++ suffix)
-    | n         => Name.mkStr n suffix
+    | str p s => Name.mkStr p (s ++ suffix)
+    | n       => Name.mkStr n suffix
 
 @[export lean_name_append_index_after]
 def appendIndexAfter (n : Name) (idx : Nat) : Name :=
   n.modifyBase fun
-    | str p s _ => Name.mkStr p (s ++ "_" ++ toString idx)
-    | n         => Name.mkStr n ("_" ++ toString idx)
+    | str p s => Name.mkStr p (s ++ "_" ++ toString idx)
+    | n       => Name.mkStr n ("_" ++ toString idx)
 
 @[export lean_name_append_before]
 def appendBefore (n : Name) (pre : String) : Name :=
   n.modifyBase fun
     | anonymous => Name.mkStr anonymous pre
-    | str p s _ => Name.mkStr p (pre ++ s)
-    | num p n _ => Name.mkNum (Name.mkStr p pre) n
+    | str p s => Name.mkStr p (pre ++ s)
+    | num p n => Name.mkNum (Name.mkStr p pre) n
+
+protected theorem beq_iff_eq {m n : Name} : m == n ↔ m = n := by
+  show m.beq n ↔ _
+  induction m generalizing n <;> cases n <;> simp_all [Name.beq, And.comm]
+
+instance : LawfulBEq Name where
+  eq_of_beq := Name.beq_iff_eq.1
+  rfl := Name.beq_iff_eq.2 rfl
+
+instance : DecidableEq Name :=
+  fun a b => if h : a == b then .isTrue (by simp_all) else .isFalse (by simp_all)
 
 end Name
 
@@ -920,15 +931,15 @@ instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[qu
 -- in contrast to `Name.toString`, we can, and want to be, precise here
 private def getEscapedNameParts? (acc : List String) : Name → Option (List String)
   | Name.anonymous => if acc.isEmpty then none else some acc
-  | Name.str n s _ => do
+  | Name.str n s => do
     let s ← Name.escapePart s
     getEscapedNameParts? (s::acc) n
-  | Name.num _ _ _ => none
+  | Name.num _ _ => none
 
 def quoteNameMk : Name → Term
   | Name.anonymous => mkCIdent ``Name.anonymous
-  | Name.str n s _ => Syntax.mkCApp ``Name.mkStr #[quoteNameMk n, quote s]
-  | Name.num n i _ => Syntax.mkCApp ``Name.mkNum #[quoteNameMk n, quote i]
+  | Name.str n s => Syntax.mkCApp ``Name.mkStr #[quoteNameMk n, quote s]
+  | Name.num n i => Syntax.mkCApp ``Name.mkNum #[quoteNameMk n, quote i]
 
 instance : Quote Name `term where
   quote n := match getEscapedNameParts? [] n with
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index f784cc7562..01c00a93d8 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1747,47 +1747,47 @@ namespace Lean
 /- Hierarchical names -/
 inductive Name where
   | anonymous : Name
-  | str : Name → String → UInt64 → Name
-  | num : Name → Nat → UInt64 → Name
+  | str : Name → String → Name
+  | num : Name → Nat → Name
+with
+  @[computedField] hash : Name → UInt64
+    | .anonymous => .ofNatCore 1723 (by decide)
+    | .str p s => mixHash p.hash s.hash
+    | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide)))
 
 instance : Inhabited Name where
   default := Name.anonymous
 
-protected def Name.hash : Name → UInt64
-  | Name.anonymous => UInt64.ofNatCore 1723 (by decide)
-  | Name.str _ _ h => h
-  | Name.num _ _ h => h
-
 instance : Hashable Name where
   hash := Name.hash
 
 namespace Name
 
 @[export lean_name_mk_string]
-def mkStr (p : Name) (s : String) : Name :=
-  Name.str p s (mixHash (hash p) (hash s))
+abbrev mkStr (p : Name) (s : String) : Name :=
+  Name.str p s
 
 @[export lean_name_mk_numeral]
-def mkNum (p : Name) (v : Nat) : Name :=
-  Name.num p v (mixHash (hash p) (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide))))
+abbrev mkNum (p : Name) (v : Nat) : Name :=
+  Name.num p v
 
-def mkSimple (s : String) : Name :=
+abbrev mkSimple (s : String) : Name :=
   mkStr Name.anonymous s
 
 @[extern "lean_name_eq"]
 protected def beq : (@& Name) → (@& Name) → Bool
-  | anonymous,   anonymous   => true
-  | str p₁ s₁ _, str p₂ s₂ _ => and (BEq.beq s₁ s₂) (Name.beq p₁ p₂)
-  | num p₁ n₁ _, num p₂ n₂ _ => and (BEq.beq n₁ n₂) (Name.beq p₁ p₂)
-  | _,           _           => false
+  | anonymous, anonymous => true
+  | str p₁ s₁, str p₂ s₂ => and (BEq.beq s₁ s₂) (Name.beq p₁ p₂)
+  | num p₁ n₁, num p₂ n₂ => and (BEq.beq n₁ n₂) (Name.beq p₁ p₂)
+  | _,         _         => false
 
 instance : BEq Name where
   beq := Name.beq
 
 protected def append : Name → Name → Name
   | n, anonymous => n
-  | n, str p s _ => Name.mkStr (Name.append n p) s
-  | n, num p d _ => Name.mkNum (Name.append n p) d
+  | n, str p s => Name.mkStr (Name.append n p) s
+  | n, num p d => Name.mkNum (Name.append n p) d
 
 instance : Append Name where
   append := Name.append
@@ -2143,16 +2143,16 @@ The delimiter `_hyg` is used just to improve the `hasMacroScopes` performance.
 -/
 
 def Name.hasMacroScopes : Name → Bool
-  | str _ s _   => beq s "_hyg"
-  | num p _   _ => hasMacroScopes p
-  | _           => false
+  | str _ s => beq s "_hyg"
+  | num p _ => hasMacroScopes p
+  | _       => false
 
 private def eraseMacroScopesAux : Name → Name
-  | Name.str p s _   => match beq s "_@" with
+  | .str p s   => match beq s "_@" with
     | true  => p
     | false => eraseMacroScopesAux p
-  | Name.num p _ _   => eraseMacroScopesAux p
-  | Name.anonymous   => Name.anonymous
+  | .num p _   => eraseMacroScopesAux p
+  | .anonymous => Name.anonymous
 
 @[export lean_erase_macro_scopes]
 def Name.eraseMacroScopes (n : Name) : Name :=
@@ -2161,8 +2161,8 @@ def Name.eraseMacroScopes (n : Name) : Name :=
   | false => n
 
 private def simpMacroScopesAux : Name → Name
-  | Name.num p i _ => Name.mkNum (simpMacroScopesAux p) i
-  | n              => eraseMacroScopesAux n
+  | .num p i => Name.mkNum (simpMacroScopesAux p) i
+  | n        => eraseMacroScopesAux n
 
 /- Helper function we use to create binder names that do not need to be unique. -/
 @[export lean_simp_macro_scopes]
@@ -2188,30 +2188,30 @@ def MacroScopesView.review (view : MacroScopesView) : Name :=
     view.scopes.foldl Name.mkNum base
 
 private def assembleParts : List Name → Name → Name
-  | List.nil,                      acc => acc
-  | List.cons (Name.str _ s _) ps, acc => assembleParts ps (Name.mkStr acc s)
-  | List.cons (Name.num _ n _) ps, acc => assembleParts ps (Name.mkNum acc n)
-  | _,                             _   => panic "Error: unreachable @ assembleParts"
+  | .nil,                acc => acc
+  | .cons (.str _ s) ps, acc => assembleParts ps (Name.mkStr acc s)
+  | .cons (.num _ n) ps, acc => assembleParts ps (Name.mkNum acc n)
+  | _,                   _   => panic "Error: unreachable @ assembleParts"
 
 private def extractImported (scps : List MacroScope) (mainModule : Name) : Name → List Name → MacroScopesView
-  | n@(Name.str p str _), parts =>
+  | n@(Name.str p str), parts =>
     match beq str "_@" with
     | true  => { name := p, mainModule := mainModule, imported := assembleParts parts Name.anonymous, scopes := scps }
     | false => extractImported scps mainModule p (List.cons n parts)
-  | n@(Name.num p _ _), parts => extractImported scps mainModule p (List.cons n parts)
+  | n@(Name.num p _), parts => extractImported scps mainModule p (List.cons n parts)
   | _,                    _     => panic "Error: unreachable @ extractImported"
 
 private def extractMainModule (scps : List MacroScope) : Name → List Name → MacroScopesView
-  | n@(Name.str p str _), parts =>
+  | n@(Name.str p str), parts =>
     match beq str "_@" with
     | true  => { name := p, mainModule := assembleParts parts Name.anonymous, imported := Name.anonymous, scopes := scps }
     | false => extractMainModule scps p (List.cons n parts)
-  | n@(Name.num _ _ _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
+  | n@(Name.num _ _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
   | _,                    _   => panic "Error: unreachable @ extractMainModule"
 
 private def extractMacroScopesAux : Name → List MacroScope → MacroScopesView
-  | Name.num p scp _, acc => extractMacroScopesAux p (List.cons scp acc)
-  | Name.str p _   _, acc => extractMainModule acc p List.nil -- str must be "_hyg"
+  | Name.num p scp, acc => extractMacroScopesAux p (List.cons scp acc)
+  | Name.str p _  , acc => extractMainModule acc p List.nil -- str must be "_hyg"
   | _,                _   => panic "Error: unreachable @ extractMacroScopesAux"
 
 /--
diff --git a/src/Init/SizeOf.lean b/src/Init/SizeOf.lean
index 84e517d879..17682469ec 100644
--- a/src/Init/SizeOf.lean
+++ b/src/Init/SizeOf.lean
@@ -66,17 +66,17 @@ namespace Lean
    an opaque function for computing the hashcode field. -/
 protected noncomputable def Name.sizeOf : Name → Nat
   | anonymous => 1
-  | str p s _ => 1 + Name.sizeOf p + sizeOf s
-  | num p n _ => 1 + Name.sizeOf p + sizeOf n
+  | str p s   => 1 + Name.sizeOf p + sizeOf s
+  | num p n   => 1 + Name.sizeOf p + sizeOf n
 
 noncomputable instance : SizeOf Name where
   sizeOf n := n.sizeOf
 
 @[simp] theorem Name.anonymous.sizeOf_spec : sizeOf anonymous = 1 :=
   rfl
-@[simp] theorem Name.str.sizeOf_spec (p : Name) (s : String) (h : UInt64) : sizeOf (str p s h) = 1 + sizeOf p + sizeOf s :=
+@[simp] theorem Name.str.sizeOf_spec (p : Name) (s : String) : sizeOf (str p s) = 1 + sizeOf p + sizeOf s :=
   rfl
-@[simp] theorem Name.num.sizeOf_spec (p : Name) (n : Nat) (h : UInt64) : sizeOf (num p n h) = 1 + sizeOf p + sizeOf n :=
+@[simp] theorem Name.num.sizeOf_spec (p : Name) (n : Nat) : sizeOf (num p n) = 1 + sizeOf p + sizeOf n :=
   rfl
 
 deriving instance SizeOf for Syntax
diff --git a/src/Lean/AuxRecursor.lean b/src/Lean/AuxRecursor.lean
index 5c8a511196..33cfff02ed 100644
--- a/src/Lean/AuxRecursor.lean
+++ b/src/Lean/AuxRecursor.lean
@@ -35,7 +35,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
 
 def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : Name) : Bool :=
   match declName with
-  | Name.str _ s _ => s == suffix && isAuxRecursor env declName
+  | .str _ s => s == suffix && isAuxRecursor env declName
   | _ => false
 
 def isCasesOnRecursor (env : Environment) (declName : Name) : Bool :=
diff --git a/src/Lean/Compiler/ExportAttr.lean b/src/Lean/Compiler/ExportAttr.lean
index 59d7cec275..da7b9b4ca2 100644
--- a/src/Lean/Compiler/ExportAttr.lean
+++ b/src/Lean/Compiler/ExportAttr.lean
@@ -12,9 +12,9 @@ private def isValidCppId (id : String) : Bool :=
   first.isAlpha  && (id.toSubstring.drop 1).all (fun c => c.isAlpha || c.isDigit || c == '_')
 
 private def isValidCppName : Name → Bool
-  | Name.str Name.anonymous s _ => isValidCppId s
-  | Name.str p s _              => isValidCppId s && isValidCppName p
-  | _                           => false
+  | .str .anonymous s => isValidCppId s
+  | .str p s          => isValidCppId s && isValidCppName p
+  | _                 => false
 
 builtin_initialize exportAttr : ParametricAttribute Name ←
   registerParametricAttribute {
diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index 3a944a9b32..8fae3896e3 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -32,9 +32,8 @@ open Std (AssocList)
 def mkBoxedName (n : Name) : Name :=
   Name.mkStr n "_boxed"
 
-def isBoxedName : Name → Bool
-  | Name.str _ "_boxed" _ => true
-  | _                     => false
+def isBoxedName (name : Name) : Bool :=
+  name matches .str _ "_boxed"
 
 abbrev N := StateM Nat
 
diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index 267951229c..b680be6a44 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -72,9 +72,9 @@ def toCName (n : Name) : M String := do
   let env ← getEnv;
   -- TODO: we should support simple export names only
   match getExportNameFor env n with
-  | some (Name.str Name.anonymous s _) => pure s
-  | some _                             => throwInvalidExportName n
-  | none                               => if n == `main then pure leanMainFn else pure n.mangle
+  | some (.str .anonymous s) => pure s
+  | some _                   => throwInvalidExportName n
+  | none                     => if n == `main then pure leanMainFn else pure n.mangle
 
 def emitCName (n : Name) : M Unit :=
   toCName n >>= emit
@@ -83,9 +83,9 @@ def toCInitName (n : Name) : M String := do
   let env ← getEnv;
   -- TODO: we should support simple export names only
   match getExportNameFor env n with
-  | some (Name.str Name.anonymous s _) => return "_init_" ++ s
-  | some _                             => throwInvalidExportName n
-  | none                               => pure ("_init_" ++ n.mangle)
+  | some (.str .anonymous s) => return "_init_" ++ s
+  | some _                   => throwInvalidExportName n
+  | none                     => pure ("_init_" ++ n.mangle)
 
 def emitCInitName (n : Name) : M Unit :=
   toCInitName n >>= emit
diff --git a/src/Lean/Compiler/NameMangling.lean b/src/Lean/Compiler/NameMangling.lean
index 3c349f55c2..80adbb3991 100644
--- a/src/Lean/Compiler/NameMangling.lean
+++ b/src/Lean/Compiler/NameMangling.lean
@@ -48,12 +48,12 @@ namespace Lean
 
 private def Name.mangleAux : Name → String
   | Name.anonymous => ""
-  | Name.str p s _ =>
+  | Name.str p s =>
     let m := String.mangle s
     match p with
     | Name.anonymous => m
     | p              => mangleAux p ++ "_" ++ m
-  | Name.num p n _ => mangleAux p ++ "_" ++ toString n ++ "_"
+  | Name.num p n => mangleAux p ++ "_" ++ toString n ++ "_"
 
 @[export lean_name_mangle]
 def Name.mangle (n : Name) (pre : String := "l_") : String :=
diff --git a/src/Lean/Compiler/Util.lean b/src/Lean/Compiler/Util.lean
index fb11491198..7734bde973 100644
--- a/src/Lean/Compiler/Util.lean
+++ b/src/Lean/Compiler/Util.lean
@@ -65,9 +65,9 @@ def mkEagerLambdaLiftingName (n : Name) (idx : Nat) : Name :=
 
 @[export lean_is_eager_lambda_lifting_name]
 def isEagerLambdaLiftingName : Name → Bool
-  | Name.str p s _ => "_elambda".isPrefixOf s || isEagerLambdaLiftingName p
-  | Name.num p _ _ => isEagerLambdaLiftingName p
-  | _              => false
+  | .str p s => "_elambda".isPrefixOf s || isEagerLambdaLiftingName p
+  | .num p _ => isEagerLambdaLiftingName p
+  | _        => false
 
 /-- Return the name of new definitions in the a given declaration.
     Here we consider only declarations we generate code for.
@@ -97,7 +97,7 @@ def mkUnsafeRecName (declName : Name) : Name :=
 /-- Return `some _` if the given name was created using `mkUnsafeRecName` -/
 @[export lean_is_unsafe_rec_name]
 def isUnsafeRecName? : Name → Option Name
-  | Name.str n "_unsafe_rec" _ => some n
+  | .str n "_unsafe_rec" => some n
   | _ => none
 
 end Compiler
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 5c40bf852a..dcc554cd1b 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -18,58 +18,58 @@ namespace Name
 
 def getPrefix : Name → Name
   | anonymous => anonymous
-  | str p _ _ => p
-  | num p _ _ => p
+  | str p _   => p
+  | num p _   => p
 
 def getString! : Name → String
-  | str _ s _ => s
-  | _         => unreachable!
+  | str _ s => s
+  | _       => unreachable!
 
 def getNumParts : Name → Nat
   | anonymous => 0
-  | str p _ _ => getNumParts p + 1
-  | num p _ _ => getNumParts p + 1
+  | str p _   => getNumParts p + 1
+  | num p _   => getNumParts p + 1
 
 def updatePrefix : Name → Name → Name
   | anonymous, _    => anonymous
-  | str _ s _, newP => Name.mkStr newP s
-  | num _ s _, newP => Name.mkNum newP s
+  | str _ s,   newP => Name.mkStr newP s
+  | num _ s,   newP => Name.mkNum newP s
 
 def components' : Name → List Name
   | anonymous => []
-  | str n s _ => Name.mkStr anonymous s :: components' n
-  | num n v _ => Name.mkNum anonymous v :: components' n
+  | str n s   => Name.mkStr anonymous s :: components' n
+  | num n v   => Name.mkNum anonymous v :: components' n
 
 def components (n : Name) : List Name :=
   n.components'.reverse
 
 def eqStr : Name → String → Bool
-  | str anonymous s _, s' => s == s'
+  | str anonymous s, s' => s == s'
   | _,                 _  => false
 
 def isPrefixOf : Name → Name → Bool
-  | p, anonymous      => p == anonymous
-  | p, n@(num p' _ _) => p == n || isPrefixOf p p'
-  | p, n@(str p' _ _) => p == n || isPrefixOf p p'
+  | p, anonymous    => p == anonymous
+  | p, n@(num p' _) => p == n || isPrefixOf p p'
+  | p, n@(str p' _) => p == n || isPrefixOf p p'
 
 
 def isSuffixOf : Name → Name → Bool
-  | anonymous,   _           => true
-  | str p₁ s₁ _, str p₂ s₂ _ => s₁ == s₂ && isSuffixOf p₁ p₂
-  | num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && isSuffixOf p₁ p₂
-  | _,           _           => false
+  | anonymous, _         => true
+  | str p₁ s₁, str p₂ s₂ => s₁ == s₂ && isSuffixOf p₁ p₂
+  | num p₁ n₁, num p₂ n₂ => n₁ == n₂ && isSuffixOf p₁ p₂
+  | _,         _         => false
 
 def cmp : Name → Name → Ordering
-  | anonymous,   anonymous   => Ordering.eq
-  | anonymous,   _           => Ordering.lt
-  | _,           anonymous   => Ordering.gt
-  | num p₁ i₁ _, num p₂ i₂ _ =>
+  | anonymous, anonymous => Ordering.eq
+  | anonymous, _         => Ordering.lt
+  | _,         anonymous => Ordering.gt
+  | num p₁ i₁, num p₂ i₂ =>
     match cmp p₁ p₂ with
     | Ordering.eq => compare i₁ i₂
     | ord => ord
-  | num _ _ _,   str _ _ _   => Ordering.lt
-  | str _ _ _,   num _ _ _   => Ordering.gt
-  | str p₁ n₁ _, str p₂ n₂ _ =>
+  | num _ _,   str _ _   => Ordering.lt
+  | str _ _,   num _ _   => Ordering.gt
+  | str p₁ n₁, str p₂ n₂ =>
     match cmp p₁ p₂ with
     | Ordering.eq => compare n₁ n₂
     | ord => ord
@@ -78,16 +78,16 @@ def lt (x y : Name) : Bool :=
   cmp x y == Ordering.lt
 
 def quickCmpAux : Name → Name → Ordering
-  | anonymous, anonymous   => Ordering.eq
-  | anonymous, _           => Ordering.lt
-  | _,         anonymous   => Ordering.gt
-  | num n v _, num n' v' _ =>
+  | anonymous, anonymous => Ordering.eq
+  | anonymous, _         => Ordering.lt
+  | _,         anonymous => Ordering.gt
+  | num n v, num n' v' =>
     match compare v v' with
     | Ordering.eq => n.quickCmpAux n'
     | ord => ord
-  | num _ _ _, str _ _ _   => Ordering.lt
-  | str _ _ _, num _ _ _   => Ordering.gt
-  | str n s _, str n' s' _ =>
+  | num _ _, str _  _  => Ordering.lt
+  | str _ _, num _  _  => Ordering.gt
+  | str n s, str n' s' =>
     match compare s s' with
     | Ordering.eq => n.quickCmpAux n'
     | ord => ord
@@ -110,15 +110,15 @@ def quickLt (n₁ n₂ : Name) : Bool :=
 /- The frontend does not allow user declarations to start with `_` in any of its parts.
    We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
 def isInternal : Name → Bool
-  | str p s _ => s.get 0 == '_' || isInternal p
-  | num p _ _ => isInternal p
-  | _         => false
+  | str p s => s.get 0 == '_' || isInternal p
+  | num p _ => isInternal p
+  | _       => false
 
 def isAtomic : Name → Bool
-  | anonymous         => true
-  | str anonymous _ _ => true
-  | num anonymous _ _ => true
-  | _                 => false
+  | anonymous       => true
+  | str anonymous _ => true
+  | num anonymous _ => true
+  | _               => false
 
 def isAnonymous : Name → Bool
   | anonymous         => true
diff --git a/src/Lean/Data/NameTrie.lean b/src/Lean/Data/NameTrie.lean
index 113ee7e136..3fb95ee45d 100644
--- a/src/Lean/Data/NameTrie.lean
+++ b/src/Lean/Data/NameTrie.lean
@@ -34,8 +34,8 @@ private def toKey (n : Name) : List NamePart :=
   loop n []
 where
   loop
-    | Name.str p s _, parts   => loop p (NamePart.str s :: parts)
-    | Name.num p n _, parts   => loop p (NamePart.num n :: parts)
+    | Name.str p s,   parts => loop p (NamePart.str s :: parts)
+    | Name.num p n,   parts => loop p (NamePart.num n :: parts)
     | Name.anonymous, parts => parts
 
 def NameTrie.insert (t : NameTrie β) (n : Name) (b : β) : NameTrie β :=
diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index 8eac21f0cb..053dc81751 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -49,7 +49,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
   let attrName ← if attr.getKind == ``Parser.Attr.simple then
     pure attr[0].getId.eraseMacroScopes
   else match attr.getKind with
-    | Name.str _ s _ => pure <| Name.mkSimple s
+    | .str _ s => pure <| Name.mkSimple s
     | _ => throwErrorAt attr  "unknown attribute"
   unless isAttribute (← getEnv) attrName do
     throwError "unknown attribute [{attrName}]"
diff --git a/src/Lean/Elab/AutoBound.lean b/src/Lean/Elab/AutoBound.lean
index 30a15604cb..132680d439 100644
--- a/src/Lean/Elab/AutoBound.lean
+++ b/src/Lean/Elab/AutoBound.lean
@@ -39,12 +39,12 @@ Therefore, we do consider identifier with macro scopes anymore.
 
 def isValidAutoBoundImplicitName (n : Name) (relaxed : Bool) : Bool :=
   match n with
-  | Name.str Name.anonymous s _ => s.length > 0 && (relaxed || ((isGreek s.front || s.front.isLower) && isValidAutoBoundSuffix s))
+  | .str .anonymous s => s.length > 0 && (relaxed || ((isGreek s.front || s.front.isLower) && isValidAutoBoundSuffix s))
   | _ => false
 
 def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool :=
   match n with
-  | Name.str Name.anonymous s _ => s.length > 0 && (relaxed || (s.front.isLower && isValidAutoBoundSuffix s))
+  | .str .anonymous s => s.length > 0 && (relaxed || (s.front.isLower && isValidAutoBoundSuffix s))
   | _ => false
 
 end Lean.Elab
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 7bad9db25e..f5421a7f7a 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -30,8 +30,8 @@ private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header :
     activateScoped newNamespace
 
 private def addScopes (isNewNamespace : Bool) (isNoncomputable : Bool) : Name → CommandElabM Unit
-  | Name.anonymous => pure ()
-  | Name.str p header _ => do
+  | .anonymous => pure ()
+  | .str p header => do
     addScopes isNewNamespace isNoncomputable p
     let currNamespace ← getCurrNamespace
     addScope isNewNamespace isNoncomputable header (if isNewNamespace then Name.mkStr currNamespace header else currNamespace)
@@ -55,9 +55,9 @@ private def checkAnonymousScope : List Scope → Bool
   | _                           => false
 
 private def checkEndHeader : Name → List Scope → Bool
-  | Name.anonymous, _                             => true
-  | Name.str p s _, { header := h, .. } :: scopes => h == s && checkEndHeader p scopes
-  | _,              _                             => false
+  | .anonymous, _                             => true
+  | .str p s,   { header := h, .. } :: scopes => h == s && checkEndHeader p scopes
+  | _,          _                             => false
 
 @[builtinCommandElab «namespace»] def elabNamespace : CommandElab := fun stx =>
   match stx with
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 9631ec2716..bff865e8ee 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -99,7 +99,7 @@ private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) :
   let (some declName) ← getDeclName?
     | throwError "invalid `leading_parser` macro, it must be used in definitions"
   match extractMacroScopes declName with
-  | { name := Name.str _ s _, .. } =>
+  | { name := .str _ s, .. } =>
     let kind := quote declName
     let s    := quote s
     ``(withAntiquot (mkAntiquot $s $kind $(quote withAnonymousAntiquot)) (leadingNode $kind $prec $e))
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index 660ad2b29b..45d4549073 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -171,7 +171,7 @@ def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name)
     throwError "atomic identifier expected '{shortName}'"
   let declName := if isRootName then { view with name := name.replacePrefix `_root_ Name.anonymous }.review else currNamespace ++ shortName
   if isRootName then
-    let .str p s _ := name | throwError "invalid declaration name '{name}'"
+    let .str p s := name | throwError "invalid declaration name '{name}'"
     shortName := Name.mkSimple s
     currNamespace := p.replacePrefix `_root_ Name.anonymous
   checkIfShadowingStructureField declName
@@ -179,7 +179,7 @@ def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name)
   match modifiers.visibility with
   | Visibility.protected =>
     match currNamespace with
-    | Name.str _ s _ => pure (declName, Name.mkSimple s ++ shortName)
+    | .str _ s => pure (declName, Name.mkSimple s ++ shortName)
     | _ => throwError "protected declarations must be in a namespace"
   | _ => pure (declName, shortName)
 
diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean
index 881343a2f6..c16831433c 100644
--- a/src/Lean/Elab/DeclUtil.lean
+++ b/src/Lean/Elab/DeclUtil.lean
@@ -58,8 +58,8 @@ def mkFreshInstanceName (env : Environment) (nextIdx : Nat) : Name :=
 
 def isFreshInstanceName (name : Name) : Bool :=
   match name with
-  | Name.str _ s _ => "_instance".isPrefixOf s
-  | _              => false
+  | .str _ s => "_instance".isPrefixOf s
+  | _        => false
 
 /--
   Sort the given list of `usedParams` using the following order:
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 81bfbf5268..ee14792a90 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -17,12 +17,12 @@ open TSyntax.Compat
 
 private def ensureValidNamespace (name : Name) : MacroM Unit := do
   match name with
-  | Name.str p s _ =>
+  | .str p s =>
     if s == "_root_" then
       Macro.throwError s!"invalid namespace '{name}', '_root_' is a reserved namespace"
     ensureValidNamespace p
-  | Name.num _ .. => Macro.throwError s!"invalid namespace '{name}', it must not contain numeric parts"
-  | Name.anonymous => return ()
+  | .num .. => Macro.throwError s!"invalid namespace '{name}', it must not contain numeric parts"
+  | .anonymous => return ()
 
 /-- Auxiliary function for `expandDeclNamespace?` -/
 private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × Syntax)) := do
@@ -32,8 +32,8 @@ private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × S
     return none
   let scpView := extractMacroScopes id
   match scpView.name with
-  | Name.str Name.anonymous _ _ => return none
-  | Name.str pre s _            =>
+  | .str .anonymous _ => return none
+  | .str pre s        =>
     ensureValidNamespace pre
     let nameNew := { scpView with name := Name.mkSimple s }.review
     -- preserve "original" info, if any, so that hover etc. on the namespaced
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index ef30ceb698..ebd6a835cf 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -91,7 +91,7 @@ def mkInstanceName (binders : Array Syntax) (type : Syntax) : CommandElabM Name
         else if e.isSort then ref.modify (· ++ "Sort")
         else if e.isConst then
           match e.constName!.eraseMacroScopes with
-          | Name.str _ str _ =>
+          | .str _ str =>
               if str.front.isLower then
                 ref.modify (· ++ str.capitalize)
               else
diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index d75026b909..88a42872f1 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -73,8 +73,8 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
   let mut auxFunNames := #[]
   for typeName in indVal.all do
     match typeName.eraseMacroScopes with
-    | Name.str _ t _ => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
-    | _              => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
+    | .str _ t => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
+    | _        => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
   trace[Elab.Deriving.beq] "{auxFunNames}"
   let usePartial := indVal.isNested || typeInfos.size > 1
   return {
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 5043beb417..971555aa0a 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -60,7 +60,7 @@ def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name
   -- decode macro scopes from name before recursion
   let extractionResult := extractMacroScopes id
   let rec loop : Name → List String → List (Name × List String)
-    | id@(Name.str p s _), projs =>
+    | id@(.str p s), projs =>
       -- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
       let id := { extractionResult with name := id }.review
       match sectionVars.find? id with
@@ -179,7 +179,7 @@ def getQuotKind (stx : Syntax) : TermElabM SyntaxNodeKind := do
   | ``Parser.Term.attr.quot => pure `attr
   | ``Parser.Term.prio.quot => pure `prio
   | ``Parser.Term.doElem.quot => pure `doElem
-  | Name.str kind "quot" _ => return kind
+  | .str kind "quot" => return kind
   | ``dynamicQuot =>
     match (← resolveGlobalConst stx[1]) with
     | [parser] => pure parser
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 255a55a869..d2043e824a 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -425,8 +425,8 @@ private def expandParentFields (s : Struct) : TermElabM Struct := do
         else match getPathToBaseStructure? env baseStructName s.structName with
           | some path =>
             let path := path.map fun funName => match funName with
-              | .str _ s _ => .fieldName ref (Name.mkSimple s)
-              | _              => unreachable!
+              | .str _ s => .fieldName ref (Name.mkSimple s)
+              | _        => unreachable!
             return { field with lhs := path ++ field.lhs }
           | _ => throwErrorAt ref "failed to access field '{fieldName}' in parent structure"
     | _ => return field
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 97cf646f7d..2de3204c81 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -240,7 +240,7 @@ open Lean.Parser.Term hiding macroArg
 open Lean.Parser.Command
 
 private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
-  if let Name.str _ suffix _ := catName then
+  if let .str _ suffix := catName then
     let quotSymbol := "`(" ++ suffix ++ "|"
     let name := catName ++ `quot
     let cmd ← `(
@@ -297,7 +297,7 @@ where
 
   appendCatName (str : String) :=
     match catName with
-    | Name.str _ s _ => s ++ str
+    | .str _ s => s ++ str
     | _ => str
 
 /- We assume a new syntax can be treated as an atom when it starts and ends with a token.
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 1a53ae9b23..0b64715ab8 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1650,7 +1650,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
     match findLocalDecl? givenNameView (skipAuxDecl := not projs.isEmpty) with
     | some decl => some (decl.toExpr, projs)
     | none => match n with
-      | .str pre s _ => loop pre (s::projs)
+      | .str pre s => loop pre (s::projs)
       | _ => none
   return loop view.name []
 
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 2f1cf1ab1f..883232d2d5 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -75,8 +75,8 @@ def checkSyntaxNodeKind [Monad m] [MonadEnv m] [MonadError m] (k : Name) : m Nam
   else throwError "failed"
 
 def checkSyntaxNodeKindAtNamespaces [Monad m] [MonadEnv m] [MonadError m] (k : Name) : Name → m Name
-  | n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces k p
-  | Name.anonymous     => checkSyntaxNodeKind k
+  | n@(.str p _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces k p
+  | .anonymous   => checkSyntaxNodeKind k
   | _ => throwError "failed"
 
 def checkSyntaxNodeKindAtCurrentNamespaces (k : Name) : AttrM Name := do
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 5042d82a91..69fa98a89d 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -695,13 +695,13 @@ def getNamespaceSet (env : Environment) : NameSSet :=
   namespacesExt.getState env
 
 private def isNamespaceName : Name → Bool
-  | Name.str Name.anonymous _ _ => true
-  | Name.str p _ _              => isNamespaceName p
-  | _                           => false
+  | .str .anonymous _ => true
+  | .str p _          => isNamespaceName p
+  | _                 => false
 
 private def registerNamePrefixes : Environment → Name → Environment
-  | env, Name.str p _ _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env
-  | env, _              => env
+  | env, .str p _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env
+  | env, _        => env
 
 @[export lean_environment_add]
 def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean
index 5b7ff6f28d..cda2e1a112 100644
--- a/src/Lean/Hygiene.lean
+++ b/src/Lean/Hygiene.lean
@@ -51,11 +51,11 @@ private def mkInaccessibleUserNameAux (unicode : Bool) (name : Name) (idx : Nat)
     name ++ Name.mkNum "_inaccessible" idx
 
 private def mkInaccessibleUserName (unicode : Bool) : Name → Name
-  | Name.num p@(Name.str _ _ _) idx _ =>
+  | .num p@(.str ..) idx =>
     mkInaccessibleUserNameAux unicode p idx
-  | Name.num Name.anonymous idx _     =>
+  | .num .anonymous idx =>
     mkInaccessibleUserNameAux unicode Name.anonymous idx
-  | Name.num p idx _ =>
+  | .num p idx =>
     if unicode then
       (mkInaccessibleUserName unicode p).appendAfter ("⁻" ++ idx.toSuperscriptString)
     else
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index d21f092062..e061bac4e2 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -130,7 +130,7 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
   | nCtx, ctx,       tagged t d               =>
     /- Messages starting a trace context have their tags postfixed with `_traceCtx` so that
     we can detect them later. Here, we do so in order to print the trace context class. -/
-    if let Name.str cls "_traceCtx" _ := t then do
+    if let .str cls "_traceCtx" := t then do
       let d₁ ← formatAux nCtx ctx d
       return f!"[{cls}] {d₁}"
     else
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index 5fa4fd757e..2e7c4163b7 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -95,7 +95,7 @@ private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat)
     let env ← getEnv
     if !isAuxRecursor env declName then pure none
     else match declName with
-    | Name.str p s _ =>
+    | .str p s =>
       if s != recOnSuffix && s != casesOnSuffix && s != brecOnSuffix then
         pure none
       else do
diff --git a/src/Lean/Meta/ReduceEval.lean b/src/Lean/Meta/ReduceEval.lean
index a0c8c80b3d..9747bc77e4 100644
--- a/src/Lean/Meta/ReduceEval.lean
+++ b/src/Lean/Meta/ReduceEval.lean
@@ -44,11 +44,11 @@ private partial def evalName (e : Expr) : MetaM Name := do
   let Expr.const c _ _ ← pure e.getAppFn | throwFailedToEval e
   let nargs := e.getAppNumArgs
   if      c == ``Lean.Name.anonymous && nargs == 0 then pure Name.anonymous
-  else if c == ``Lean.Name.str && nargs == 3 then do
+  else if c == ``Lean.Name.str && nargs == 2 then do
     let n ← evalName $ e.getArg! 0
     let s ← reduceEval $ e.getArg! 1
     pure $ Name.mkStr n s
-  else if c == ``Lean.Name.num && nargs == 3 then do
+  else if c == ``Lean.Name.num && nargs == 2 then do
     let n ← evalName $ e.getArg! 0
     let u ← reduceEval $ e.getArg! 1
     pure $ Name.mkNum n u
diff --git a/src/Lean/Modifiers.lean b/src/Lean/Modifiers.lean
index c1d979cc99..46000614dd 100644
--- a/src/Lean/Modifiers.lean
+++ b/src/Lean/Modifiers.lean
@@ -34,17 +34,17 @@ def mkPrivateName (env : Environment) (n : Name) : Name :=
   Name.mkNum (privateHeader ++ env.mainModule) 0 ++ n
 
 def isPrivateName : Name → Bool
-  | n@(Name.str p _ _) => n == privateHeader || isPrivateName p
-  | Name.num p _ _     => isPrivateName p
-  | _                  => false
+  | n@(.str p _) => n == privateHeader || isPrivateName p
+  | .num p _     => isPrivateName p
+  | _            => false
 
 @[export lean_is_private_name]
 def isPrivateNameExport (n : Name) : Bool :=
   isPrivateName n
 
 private def privateToUserNameAux : Name → Name
-  | Name.str p s _ => Name.mkStr (privateToUserNameAux p) s
-  | _              => Name.anonymous
+  | .str p s => Name.mkStr (privateToUserNameAux p) s
+  | _        => Name.anonymous
 
 @[export lean_private_to_user_name]
 def privateToUserName? (n : Name) : Option Name :=
@@ -57,8 +57,8 @@ def isPrivateNameFromImportedModule (env : Environment) (n : Name) : Bool :=
   | _ => false
 
 private def privatePrefixAux : Name → Name
-  | Name.str p _ _ => privatePrefixAux p
-  | n              => n
+  | .str p _ => privatePrefixAux p
+  | n        => n
 
 @[export lean_private_prefix]
 def privatePrefix? (n : Name) : Option Name :=
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 3a07ce20e4..0d6854684e 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -656,7 +656,7 @@ def delabProj : Delab := do
 @[builtinDelab app]
 def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do
   let e@(Expr.app fn _ _) ← getExpr | failure
-  let Expr.const c@(Name.str _ f _) _ _ ← pure fn.getAppFn | failure
+  let .const c@(.str _ f) _ _ ← pure fn.getAppFn | failure
   let env ← getEnv
   let some info ← pure $ env.getProjectionFnInfo? c | failure
   -- can't use with classes since the instance parameter is implicit
@@ -768,18 +768,18 @@ def delabDo : Delab := whenPPOption getPPNotation do
   `(do $items:doSeqItem*)
 
 def reifyName : Expr → DelabM Name
-  | Expr.const ``Lean.Name.anonymous .. => return Name.anonymous
-  | Expr.app (Expr.app (Expr.const ``Lean.Name.mkStr ..) n _) (Expr.lit (Literal.strVal s) _) _ => return (← reifyName n).mkStr s
-  | Expr.app (Expr.app (Expr.const ``Lean.Name.mkNum ..) n _) (Expr.lit (Literal.natVal i) _) _ => return (← reifyName n).mkNum i
+  | .const ``Lean.Name.anonymous .. => return Name.anonymous
+  | .app (.app (.const ``Lean.Name.str ..) n _) (.lit (.strVal s) _) _ => return (← reifyName n).mkStr s
+  | .app (.app (.const ``Lean.Name.num ..) n _) (.lit (.natVal i) _) _ => return (← reifyName n).mkNum i
   | _ => failure
 
-@[builtinDelab app.Lean.Name.mkStr]
+@[builtinDelab app.Lean.Name.str]
 def delabNameMkStr : Delab := whenPPOption getPPNotation do
   let n ← reifyName (← getExpr)
   -- not guaranteed to be a syntactically valid name, but usually more helpful than the explicit version
   return mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{n}"]
 
-@[builtinDelab app.Lean.Name.mkNum]
+@[builtinDelab app.Lean.Name.num]
 def delabNameMkNum : Delab := delabNameMkStr
 
 end Lean.PrettyPrinter.Delaborator
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index a713d9c7c7..624eb3ed7d 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -71,7 +71,7 @@ private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : L
 
 /- Check surrounding namespaces -/
 private def resolveUsingNamespace (env : Environment) (id : Name) : Name → List Name
-  | ns@(Name.str p _ _) =>
+  | ns@(.str p _) =>
     match resolveQualifiedName env ns id with
     | []          => resolveUsingNamespace env id p
     | resolvedIds => resolvedIds
@@ -118,7 +118,7 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
   let extractionResult := extractMacroScopes id
   let rec loop (id : Name) (projs : List String) : List (Name × List String) :=
     match id with
-    | Name.str p s _ =>
+    | .str p s =>
       -- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
       let id := { extractionResult with name := id }.review
       match resolveUsingNamespace env id ns with
@@ -141,9 +141,9 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
 /- Namespace resolution -/
 
 def resolveNamespaceUsingScope? (env : Environment) (n : Name) : Name → Option Name
-  | Name.anonymous      => if env.isNamespace n then some n else none
-  | ns@(Name.str p _ _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope? env n p
-  | _                   => unreachable!
+  | .anonymous    => if env.isNamespace n then some n else none
+  | ns@(.str p _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope? env n p
+  | _             => unreachable!
 
 def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → List Name
   | []                          => []
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index 0afa85b689..c4bfcd1a05 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -124,7 +124,7 @@ private def runM (ctx : ContextInfo) (lctx : LocalContext) (x : M Unit) : IO (Op
 
 private def matchAtomic (id : Name) (declName : Name) : Option Float :=
   match id, declName with
-  | Name.str Name.anonymous s₁ _, Name.str Name.anonymous s₂ _ => fuzzyMatchScoreWithThreshold? s₁ s₂
+  | .str .anonymous s₁, .str .anonymous s₂ => fuzzyMatchScoreWithThreshold? s₁ s₂
   | _, _ => none
 
 private def normPrivateName (declName : Name) : MetaM Name := do
@@ -157,7 +157,7 @@ private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName :
         return none
     else if !danglingDot then
       match id, declName with
-      | Name.str p₁ s₁ _, Name.str p₂ s₂ _ =>
+      | .str p₁ s₁, .str p₂ s₂ =>
         if p₁ == p₂  then
           return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (s₂, ·)
         else
@@ -175,7 +175,7 @@ private partial def truncate (id : Name) (newLen : Nat) : Name :=
      match id with
      | Name.anonymous => (id, 0)
      | Name.num ..    => unreachable!
-     | Name.str p s _ =>
+     | .str p s =>
        let (p', len) := go p
        if len + 1 >= newLen then
          (p', len)
@@ -200,7 +200,7 @@ def matchNamespace (ns : Name) (nsFragment : Name) (danglingDot : Bool) : Option
       none
   else
     match ns, nsFragment with
-    | Name.str p₁ s₁ _, Name.str p₂ s₂ _ =>
+    | .str p₁ s₁, .str p₂ s₂ =>
       if p₁ == p₂ then fuzzyMatchScoreWithThreshold? s₂ s₁ else none
     | _, _ => none
 
@@ -304,7 +304,7 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI
         | _ => return ()
     searchAlias ctx.currNamespace
   -- Search keywords
-  if let Name.str Name.anonymous s _ := id then
+  if let .str .anonymous s := id then
     let keywords := Parser.getTokenTable env
     for keyword in keywords.findPrefix s do
       addKeywordCompletionItem keyword
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index f0e603d66f..24fc5ba7c2 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -367,7 +367,7 @@ namespace Syntax
 
 -- quotation node kinds are formed from a unique quotation name plus "quot"
 def isQuot : Syntax → Bool
-  | Syntax.node _ (Name.str _ "quot" _)         _ => true
+  | Syntax.node _ (Name.str _ "quot")           _ => true
   | Syntax.node _ `Lean.Parser.Term.dynamicQuot _ => true
   | _                                             => false
 
@@ -380,8 +380,8 @@ def getQuotContent (stx : Syntax) : Syntax :=
 
 -- antiquotation node kinds are formed from the original node kind (if any) plus "antiquot"
 def isAntiquot : Syntax → Bool
-  | Syntax.node _ (Name.str _ "antiquot" _) _ => true
-  | _                                         => false
+  | .node _ (.str _ "antiquot") _ => true
+  | _                             => false
 
 def isAntiquots (stx : Syntax) : Bool :=
   stx.isAntiquot || (stx.isOfKind choiceKind && stx.getNumArgs > 0 && stx.getArgs.all isAntiquot)
@@ -425,9 +425,9 @@ def getAntiquotTerm (stx : Syntax) : Syntax :=
 
 /-- Return kind of parser expected at this antiquotation, and whether it is a "pseudo" kind (see `mkAntiquot`). -/
 def antiquotKind? : Syntax → Option (SyntaxNodeKind × Bool)
-  | Syntax.node _ (Name.str (Name.str k "pseudo" _) "antiquot" _) _ => (k, true)
-  | Syntax.node _ (Name.str k                       "antiquot" _) _ => (k, false)
-  | _                                                               => none
+  | .node _ (.str (.str k "pseudo") "antiquot") _ => (k, true)
+  | .node _ (.str k                 "antiquot") _ => (k, false)
+  | _                                             => none
 
 def antiquotKinds (stx : Syntax) : List (SyntaxNodeKind × Bool) :=
   if stx.isOfKind choiceKind then
@@ -439,7 +439,7 @@ def antiquotKinds (stx : Syntax) : List (SyntaxNodeKind × Bool) :=
 
 -- An "antiquotation splice" is something like `$[...]?` or `$[...]*`.
 def antiquotSpliceKind? : Syntax → Option SyntaxNodeKind
-  | Syntax.node _ (Name.str k "antiquot_scope" _) _ => some k
+  | .node _ (.str k "antiquot_scope") _ => some k
   | _ => none
 
 def isAntiquotSplice (stx : Syntax) : Bool :=
@@ -461,7 +461,7 @@ def mkAntiquotSpliceNode (kind : SyntaxNodeKind) (contents : Array Syntax) (suff
 
 -- `$x,*` etc.
 def antiquotSuffixSplice? : Syntax → Option SyntaxNodeKind
-  | Syntax.node _ (Name.str k "antiquot_suffix_splice" _) _ => some k
+  | .node _ (.str k "antiquot_suffix_splice") _ => some k
   | _ => none
 
 def isAntiquotSuffixSplice (stx : Syntax) : Bool :=
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index 8b19edd1d0..6091a0a152 100644
--- a/src/Lean/Util/Path.lean
+++ b/src/Lean/Util/Path.lean
@@ -20,9 +20,9 @@ def modToFilePath (base : FilePath) (mod : Name) (ext : String) : FilePath :=
   go mod |>.withExtension ext
 where
   go : Name → FilePath
-  | Name.str p h _ => go p / h
+  | Name.str p h => go p / h
   | Name.anonymous => base
-  | Name.num _ _ _ => panic! "ill-formed import"
+  | Name.num _ _ => panic! "ill-formed import"
 
 /-- A `.olean' search path. -/
 abbrev SearchPath := System.SearchPath
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 35d7a95a37..7d0af33302 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -54,8 +54,8 @@ def resetTraceState {m} [MonadTrace m] : m Unit :=
   modifyTraceState (fun _ => {})
 
 private def checkTraceOptionAux (opts : Options) : Name → Bool
-  | n@(Name.str p _ _) => opts.getBool n || (!opts.contains n && checkTraceOptionAux opts p)
-  | _                  => false
+  | n@(.str p _) => opts.getBool n || (!opts.contains n && checkTraceOptionAux opts p)
+  | _            => false
 
 def checkTraceOption (opts : Options) (cls : Name) : Bool :=
   if opts.isEmpty then false
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 5f5cb08b90..74265f3b99 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -106,7 +106,7 @@ where
   | _,    ctx,       withNamingContext nCtx d => go nCtx ctx d
   | nCtx, ctx,       tagged t d               => do
     -- We postfix trace contexts with `_traceCtx` in order to detect them in messages.
-    if let Name.str cls "_traceCtx" _ := t then
+    if let .str cls "_traceCtx" := t then
       -- When interactive trace exploration is possible, we hide traces which can otherwise
       -- take significant resources to pretty-print.
       if hasWidgets then
diff --git a/src/lake b/src/lake
index 35cc869b01..0d6e16a3ad 160000
--- a/src/lake
+++ b/src/lake
@@ -1 +1 @@
-Subproject commit 35cc869b018e41a0dbaf74ed07c8ec9cf1ee4ac3
+Subproject commit 0d6e16a3ad6b0e190b1d557df86fc627d4597c29
diff --git a/tests/lean/namelit.lean.expected.out b/tests/lean/namelit.lean.expected.out
index 54caade097..188f2ea44b 100644
--- a/tests/lean/namelit.lean.expected.out
+++ b/tests/lean/namelit.lean.expected.out
@@ -1,8 +1,8 @@
-Lean.Name.mkStr Lean.Name.anonymous "foo" : Lean.Name
-Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo") "bla" : Lean.Name
-Lean.Name.mkStr Lean.Name.anonymous "foo bla" : Lean.Name
-Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo bla") "hello world" : Lean.Name
-Lean.Name.mkStr (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo bla") "boo") "hello world" : Lean.Name
-Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "foo") "hello" : Lean.Name
-Lean.Name.mkStr Lean.Name.anonymous "hello" : Lean.Name
-Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "hello") "world !!!" : Lean.Name
+Lean.Name.str Lean.Name.anonymous "foo" : Lean.Name
+Lean.Name.str (Lean.Name.str Lean.Name.anonymous "foo") "bla" : Lean.Name
+Lean.Name.str Lean.Name.anonymous "foo bla" : Lean.Name
+Lean.Name.str (Lean.Name.str Lean.Name.anonymous "foo bla") "hello world" : Lean.Name
+Lean.Name.str (Lean.Name.str (Lean.Name.str Lean.Name.anonymous "foo bla") "boo") "hello world" : Lean.Name
+Lean.Name.str (Lean.Name.str Lean.Name.anonymous "foo") "hello" : Lean.Name
+Lean.Name.str Lean.Name.anonymous "hello" : Lean.Name
+Lean.Name.str (Lean.Name.str Lean.Name.anonymous "hello") "world !!!" : Lean.Name
diff --git a/tests/lean/run/998Export.lean b/tests/lean/run/998Export.lean
index c48d70ffed..b6a2384f2b 100644
--- a/tests/lean/run/998Export.lean
+++ b/tests/lean/run/998Export.lean
@@ -55,9 +55,9 @@ def exportName (n : Name) : ExportM Nat := do
   match (← get).names.map.find? n with
   | some i => pure i
   | none => match n with
-    | Name.anonymous => pure 0
-    | Name.num p a _ => let i ← alloc n; IO.println s!"{i} #NI {← exportName p} {a}"; pure i
-    | Name.str p s _ => let i ← alloc n; IO.println s!"{i} #NS {← exportName p} {s}"; pure i
+    | .anonymous => pure 0
+    | .num p a => let i ← alloc n; IO.println s!"{i} #NI {← exportName p} {a}"; pure i
+    | .str p s => let i ← alloc n; IO.println s!"{i} #NS {← exportName p} {s}"; pure i
 
 attribute [simp] exportName
 
diff --git a/tests/lean/run/printDecls.lean b/tests/lean/run/printDecls.lean
index 6685048aa6..6006ce421f 100644
--- a/tests/lean/run/printDecls.lean
+++ b/tests/lean/run/printDecls.lean
@@ -7,7 +7,7 @@ open Lean.Meta
 def shouldIgnore (declName : Name) : Bool :=
   declName.isInternal
   || match declName with
-     | Name.str _ s _ => "match_".isPrefixOf s || "proof_".isPrefixOf s || "eq_".isPrefixOf s
+     | .str _ s => "match_".isPrefixOf s || "proof_".isPrefixOf s || "eq_".isPrefixOf s
      | _ => true
 
 -- Print declarations that have the given prefix.