From cdbe29b46d35ca1d16affa329813e8d7d41dfe7e Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Tue, 29 Oct 2024 09:43:11 -0700
Subject: [PATCH] feat: accurate binder names in signatures (like in output of
 `#check`) (#5827)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

An important part of the interface of a function is the parameter names,
for making used of named arguments. This PR makes the parameter names
print in a reliable way. The parameters of the type now appear as
hygienic names if they cannot be used as named arguments.

Modifies the heuristic for how parameters are chosen to appear before or
after the colon. The rule is now that parameters start appearing after
the colon at the first non-dependent non-instance-implicit parameter
that has a name unusable as a named argument. This is a refinement of
#2846.

Fixes the issue where consecutive hygienic names pretty print without a
space separating them, so we now have `(x✝ y✝ : Nat)` rather than `(x✝y✝
: Nat)`.

Breaking change: `Lean.PrettyPrinter.Formatter.pushToken` now takes an
additional boolean `ident` argument, which should be `true` for
identifiers. Used to insert discretionary space between consecutive
identifiers.

Closes #5810
---
 src/Lean/PrettyPrinter/Delaborator/Basic.lean | 32 ++++++--
 .../PrettyPrinter/Delaborator/Builtins.lean   | 51 +++++++++---
 .../PrettyPrinter/Delaborator/SubExpr.lean    |  8 ++
 src/Lean/PrettyPrinter/Formatter.lean         | 65 +++++++++------
 src/lake/Lake/Toml/ParserUtil.lean            |  2 +-
 ...toImplicitChainNameIssue.lean.expected.out |  2 +-
 tests/lean/match1.lean.expected.out           |  4 +-
 tests/lean/run/2846.lean                      | 26 ++++--
 tests/lean/run/4320.lean                      |  2 +-
 tests/lean/run/5424.lean                      | 10 +++
 tests/lean/run/974.lean                       | 15 ++--
 tests/lean/run/eqnsPrio.lean                  |  4 +-
 tests/lean/run/funind_demo.lean               |  6 +-
 tests/lean/run/funind_fewer_levels.lean       |  8 +-
 tests/lean/run/funind_proof.lean              |  2 +-
 tests/lean/run/funind_structural.lean         | 18 ++--
 tests/lean/run/funind_structural_mutual.lean  |  4 +-
 tests/lean/run/funind_tests.lean              | 82 +++++++++----------
 tests/lean/run/namePatEqThm.lean              |  6 +-
 tests/lean/run/reserved.lean                  | 22 +++--
 tests/lean/run/structuralMutual.lean          | 12 +--
 tests/lean/run/unfoldLemma.lean               | 11 ++-
 tests/lean/run/wfEqns5.lean                   | 68 ++++++++-------
 23 files changed, 269 insertions(+), 191 deletions(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index bf0de8759e..805044fcb8 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -228,14 +228,27 @@ def withAnnotateTermInfo (d : Delab) : Delab := do
   let stx ← d
   annotateTermInfo stx
 
-def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do
-  -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
-  let suggestion := if suggestion.isAnonymous then `a else suggestion
-  -- We use this small hack to convert identifiers created using `mkAuxFunDiscr` to simple names
-  let suggestion := suggestion.eraseMacroScopes
+/--
+Gets an name based on `suggestion` that is unused in the local context.
+Erases macro scopes.
+If `pp.safeShadowing` is true, then the name is allowed to shadow a name in the local context
+if the name does not appear in `body`.
+
+If `preserveName` is false, then returns the name, possibly with fresh macro scopes added.
+If `suggestion` has macro scopes then the result does as well.
+-/
+def getUnusedName (suggestion : Name) (body : Expr) (preserveName : Bool := false) : DelabM Name := do
+  let (hasScopes, suggestion) :=
+    if suggestion.isAnonymous then
+      -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
+      (true, `a)
+    else
+      (suggestion.hasMacroScopes, suggestion.eraseMacroScopes)
   let lctx ← getLCtx
-  if !lctx.usesUserName suggestion then
+  if !lctx.usesUserName suggestion || (preserveName && !hasScopes) then
     return suggestion
+  else if preserveName then
+    withFreshMacroScope <| MonadQuotation.addMacroScope suggestion
   else if (← getPPOption getPPSafeShadowing) && !bodyUsesSuggestion lctx suggestion then
     return suggestion
   else
@@ -262,9 +275,12 @@ def mkAnnotatedIdent (n : Name) (e : Expr) : DelabM Ident := do
 Enters the body of the current expression, which must be a lambda or forall.
 The binding variable is passed to `d` as `Syntax`, and it is an identifier that has been annotated with the fvar expression
 for the variable.
+
+If `preserveName` is `false` (the default), gives the binder an unused name.
+Otherwise, it tries to preserve the textual form of the name, preserving whether it is hygienic.
 -/
-def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) : DelabM α := do
-  let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody!
+def withBindingBodyUnusedName {α} (d : Syntax → DelabM α) (preserveName := false) : DelabM α := do
+  let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody! (preserveName := preserveName)
   withBindingBody' n (mkAnnotatedIdent n) (d ·)
 
 inductive OmissionReason
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 17e0d219e5..138bde803b 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -887,24 +887,31 @@ def delabLam : Delab :=
       else
         `(fun $binders* => $stxBody)
 
+/-- Don't do any renaming for forall binders, but do add fresh macro scopes when there is shadowing. -/
+private def ppPiPreserveNames := `pp.piPreserveNames
+/-- Causes non-dependent foralls to print with binder names. -/
+private def ppPiBinderNames := `pp.piBinderNames
+
 /--
 Similar to `delabBinders`, but tracking whether `forallE` is dependent or not.
 
 See issue #1571
 -/
 private partial def delabForallBinders (delabGroup : Array Syntax → Bool → Syntax → Delab) (curNames : Array Syntax := #[]) (curDep := false) : Delab := do
-  let dep := !(← getExpr).isArrow
+  -- Logic note: wanting to print with binder names is equivalent to pretending the forall is dependent.
+  let dep := !(← getExpr).isArrow || (← getOptionsAtCurrPos).get ppPiBinderNames false
   if !curNames.isEmpty && dep != curDep then
     -- don't group
     delabGroup curNames curDep (← delab)
   else
+    let preserve := (← getOptionsAtCurrPos).get ppPiPreserveNames false
     let curDep := dep
     if ← shouldGroupWithNext then
       -- group with nested binder => recurse immediately
-      withBindingBodyUnusedName fun stxN => delabForallBinders delabGroup (curNames.push stxN) curDep
+      withBindingBodyUnusedName (preserveName := preserve) fun stxN => delabForallBinders delabGroup (curNames.push stxN) curDep
     else
       -- don't group => delab body and prepend current binder group
-      let (stx, stxN) ← withBindingBodyUnusedName fun stxN => return (← delab, stxN)
+      let (stx, stxN) ← withBindingBodyUnusedName (preserveName := preserve) fun stxN => return (← delab, stxN)
       delabGroup (curNames.push stxN) curDep stx
 
 @[builtin_delab forallE]
@@ -1297,11 +1304,13 @@ where
       -- but this would be the usual case.
       let group ← withBindingDomain do `(bracketedBinderF|[$(← delabTy)])
       withBindingBody e.bindingName! <| delabParams bindingNames idStx (groups.push group)
-    else if e.isForall && !e.bindingName!.hasMacroScopes && !bindingNames.contains e.bindingName! then
+    else if e.isForall && (!e.isArrow || !(e.bindingName!.hasMacroScopes || bindingNames.contains e.bindingName!)) then
       delabParamsAux bindingNames idStx groups #[]
     else
-      let type ← delabTy
-      `(declSigWithId| $idStx:ident $groups* : $type)
+      let (opts', e') ← processSpine {} (← readThe SubExpr)
+      withReader (fun ctx => {ctx with optionsPerPos := opts', subExpr := { ctx.subExpr with expr := e' }}) do
+        let type ← delabTy
+        `(declSigWithId| $idStx:ident $groups* : $type)
   /--
   Inner loop for `delabParams`, collecting binders.
   Invariants:
@@ -1311,6 +1320,7 @@ where
   -/
   delabParamsAux (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
     let e@(.forallE n d e' i) ← getExpr | unreachable!
+    let n ← if bindingNames.contains n then withFreshMacroScope <| MonadQuotation.addMacroScope n else pure n
     let bindingNames := bindingNames.insert n
     let stxN := mkIdent n
     let curIds := curIds.push ⟨stxN⟩
@@ -1336,13 +1346,34 @@ where
   -/
   shouldGroupWithNext (bindingNames : NameSet) (e e' : Expr) : Bool :=
     e'.isForall &&
-    -- At the first sign of an inaccessible name, stop merging binders:
-    !e'.bindingName!.hasMacroScopes &&
-    -- If it's a name that has already been used, stop merging binders:
-    !bindingNames.contains e'.bindingName! &&
+    (!e'.isArrow ||
+      -- At the first sign of an inaccessible name, stop merging binders:
+    !(e'.bindingName!.hasMacroScopes ||
+      -- If it's a name that has already been used, stop merging binders:
+      bindingNames.contains e'.bindingName!)) &&
     e.binderInfo == e'.binderInfo &&
     e.bindingDomain! == e'.bindingDomain! &&
     -- Inst implicits can't be grouped:
     e'.binderInfo != BinderInfo.instImplicit
+  /--
+  Go through rest of type, alpha renaming and setting options along the spine.
+  -/
+  processSpine (opts : OptionsPerPos) (subExpr : SubExpr) : MetaM (OptionsPerPos × Expr) := do
+    if let .forallE n t b bi := subExpr.expr then
+      let used := (← getLCtx).usesUserName n
+      withLocalDecl n bi t fun fvar => do
+        let (opts, b') ← processSpine opts { expr := b.instantiate1 fvar, pos := subExpr.pos.pushBindingBody }
+        let b' := b'.abstract #[fvar]
+        let opts := opts.insertAt subExpr.pos ppPiPreserveNames true
+        if n.hasMacroScopes then
+          return (opts, .forallE n t b' bi)
+        else if !used then
+          let opts := opts.insertAt subExpr.pos ppPiBinderNames true
+          return (opts, .forallE n t b' bi)
+        else
+          let n' ← withFreshMacroScope <| MonadQuotation.addMacroScope n
+          return (opts, .forallE n' t b' bi)
+    else
+      return (opts, subExpr.expr)
 
 end Lean.PrettyPrinter.Delaborator
diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
index dfa8311f3e..30909660e4 100644
--- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
@@ -18,6 +18,14 @@ namespace Lean.PrettyPrinter.Delaborator
 
 abbrev OptionsPerPos := RBMap SubExpr.Pos Options compare
 
+def OptionsPerPos.insertAt (optionsPerPos : OptionsPerPos) (pos : SubExpr.Pos) (name : Name) (value : DataValue) : OptionsPerPos :=
+  let opts := optionsPerPos.find? pos |>.getD {}
+  optionsPerPos.insert pos <| opts.insert name value
+
+/-- Merges two collections of options, where the second overrides the first. -/
+def OptionsPerPos.merge : OptionsPerPos → OptionsPerPos → OptionsPerPos :=
+  RBMap.mergeBy (fun _ => KVMap.mergeBy (fun _ _ dv => dv))
+
 namespace SubExpr
 
 open Lean.SubExpr
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 8b9324fe3d..23f7ec3042 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -30,16 +30,18 @@ structure Context where
 
 structure State where
   stxTrav  : Syntax.Traverser
-  -- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual
-  -- content of `stack` is modified only by `pushText` and `pushLine`, so `leadWord` is adjusted there accordingly.
+  /-- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual
+  content of `stack` is modified only by `pushText` and `pushLine`, so `leadWord` is adjusted there accordingly. -/
   leadWord : String := ""
-  -- Whether the generated format begins with the result of an ungrouped category formatter.
+  /-- When the `leadWord` is nonempty, whether it is an identifier. Identifiers get space inserted between them. -/
+  leadWordIdent : Bool := false
+  /-- Whether the generated format begins with the result of an ungrouped category formatter. -/
   isUngrouped : Bool := false
-  -- Whether the resulting format must be grouped when used in a category formatter.
-  -- If the flag is set to false, then categoryParser omits the fill+nest operation.
+  /-- Whether the resulting format must be grouped when used in a category formatter.
+  If the flag is set to false, then categoryParser omits the fill+nest operation. -/
   mustBeGrouped : Bool := true
-  -- Stack of generated Format objects, analogous to the Syntax stack in the parser.
-  -- Note, however, that the stack is reversed because of the right-to-left traversal.
+  /-- Stack of generated Format objects, analogous to the Syntax stack in the parser.
+  Note, however, that the stack is reversed because of the right-to-left traversal. -/
   stack    : Array Format := #[]
 
 end Formatter
@@ -121,7 +123,7 @@ private def push (f : Format) : FormatterM Unit :=
 
 def pushWhitespace (f : Format) : FormatterM Unit := do
   push f
-  modify fun st => { st with leadWord := "", isUngrouped := false }
+  modify fun st => { st with leadWord := "", leadWordIdent := false, isUngrouped := false }
 
 def pushLine : FormatterM Unit :=
   pushWhitespace Format.line
@@ -335,7 +337,7 @@ def parseToken (s : String) : FormatterM ParserState :=
     options := ← getOptions
   } ((← read).table) (Parser.mkParserState s)
 
-def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
+def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit := do
   match info with
   | SourceInfo.original _ _ ss _ =>
     -- preserve non-whitespace content (i.e. comments)
@@ -346,23 +348,34 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
         push s!"\n{ss'}"
       else
         push s!"  {ss'}"
-      modify fun st => { st with leadWord := "" }
+      modify fun st => { st with leadWord := "", leadWordIdent := false }
   | _ => pure ()
 
   let st ← get
-  -- If there is no space between `tk` and the next word, see if we would parse more than `tk` as a single token
+  -- If there is no space between `tk` and the next word, see if we should insert a discretionary space.
   if st.leadWord != "" && tk.trimRight == tk then
-    let tk' := tk.trimLeft
-    let t ← parseToken $ tk' ++ st.leadWord
-    if t.pos <= tk'.endPos then
-      -- stopped within `tk` => use it as is, extend `leadWord` if not prefixed by whitespace
+    let insertSpace ← do
+      if ident && st.leadWordIdent then
+        -- Both idents => need space
+        pure true
+      else
+        -- Check if we would parse more than `tk` as a single token
+        let tk' := tk.trimLeft
+        let t ← parseToken $ tk' ++ st.leadWord
+        if t.pos ≤ tk'.endPos then
+          -- stopped within `tk` => use it as is
+          pure false
+        else
+          -- stopped after `tk` => add space
+          pure true
+    if !insertSpace then
+      -- extend `leadWord` if not prefixed by whitespace
       push tk
-      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "" }
+      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "", leadWordIdent := ident }
     else
-      -- stopped after `tk` => add space
       pushLine
       push tk
-      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
+      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "", leadWordIdent := ident }
   else
     -- already separated => use `tk` as is
     if st.leadWord == "" then
@@ -372,7 +385,7 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
       push tk.trimRight
     else
       push tk -- preserve special whitespace for tokens like ":=\n"
-    modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
+    modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "", leadWordIdent := ident }
 
   match info with
   | SourceInfo.original ss _ _ _ =>
@@ -395,7 +408,7 @@ def symbolNoAntiquot.formatter (sym : String) : Formatter := do
   let stx ← getCur
   if stx.isToken sym then do
     let (Syntax.atom info _) ← pure stx | unreachable!
-    withMaybeTag (getExprPos? stx) (pushToken info sym)
+    withMaybeTag (getExprPos? stx) (pushToken info sym false)
     goLeft
   else do
     trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected symbol '{sym}'"
@@ -410,9 +423,9 @@ def unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter := do
   let Syntax.atom info val ← getCur
     | throwError m!"not an atom: {← getCur}"
   if val == sym.trim then
-    pushToken info sym
+    pushToken info sym false
   else
-    pushToken info asciiSym;
+    pushToken info asciiSym false
   goLeft
 
 @[combinator_formatter identNoAntiquot]
@@ -423,14 +436,14 @@ def identNoAntiquot.formatter : Formatter := do
   let id := id.simpMacroScopes
   let table := (← read).table
   let isToken (s : String) : Bool := (table.find? s).isSome
-  withMaybeTag (getExprPos? stx) (pushToken info (id.toString (isToken := isToken)))
+  withMaybeTag (getExprPos? stx) (pushToken info (id.toString (isToken := isToken)) true)
   goLeft
 
 @[combinator_formatter rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do
   checkKind identKind
   let Syntax.ident info _ id _ ← getCur
     | throwError m!"not an ident: {← getCur}"
-  pushToken info id.toString
+  pushToken info id.toString true
   goLeft
 
 @[combinator_formatter identEq] def identEq.formatter (_id : Name) := rawIdentNoAntiquot.formatter
@@ -441,7 +454,7 @@ def visitAtom (k : SyntaxNodeKind) : Formatter := do
     checkKind k
   let Syntax.atom info val ← pure $ stx.ifNode (fun n => n.getArg 0) (fun _ => stx)
     | throwError m!"not an atom: {stx}"
-  pushToken info val
+  pushToken info val false
   goLeft
 
 @[combinator_formatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind
@@ -490,7 +503,7 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
 @[combinator_formatter checkStackTop] def checkStackTop.formatter : Formatter := pure ()
 @[combinator_formatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter :=
   -- prevent automatic whitespace insertion
-  modify fun st => { st with leadWord := "" }
+  modify fun st => { st with leadWord := "", leadWordIdent := false }
 @[combinator_formatter checkLinebreakBefore] def checkLinebreakBefore.formatter : Formatter := pure ()
 @[combinator_formatter checkTailWs] def checkTailWs.formatter : Formatter := pure ()
 @[combinator_formatter checkColEq] def checkColEq.formatter : Formatter := pure ()
diff --git a/src/lake/Lake/Toml/ParserUtil.lean b/src/lake/Lake/Toml/ParserUtil.lean
index 43e3d2070e..de874dc035 100644
--- a/src/lake/Lake/Toml/ParserUtil.lean
+++ b/src/lake/Lake/Toml/ParserUtil.lean
@@ -161,7 +161,7 @@ open Formatter Syntax.MonadTraverser in
   let .atom info val := stx
     | trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected atom"
       throwBacktrack
-  withMaybeTag (getSyntaxExprPos? stx) (pushToken info val)
+  withMaybeTag (getSyntaxExprPos? stx) (pushToken info val false)
   goLeft
 
 @[combinator_parenthesizer atom]
diff --git a/tests/lean/autoImplicitChainNameIssue.lean.expected.out b/tests/lean/autoImplicitChainNameIssue.lean.expected.out
index 749246019c..a56d97e58d 100644
--- a/tests/lean/autoImplicitChainNameIssue.lean.expected.out
+++ b/tests/lean/autoImplicitChainNameIssue.lean.expected.out
@@ -3,4 +3,4 @@ case nil
 α✝ : Type u_1
 as : List α✝
 ⊢ Palindrome [].reverse
-palindrome_reverse.{u_1} : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome as.reverse
+palindrome_reverse.{u_1} {α✝ : Type u_1} {as : List α✝} (h : Palindrome as) : Palindrome as.reverse
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index 14f9bcfa50..c5afb1731d 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -46,6 +46,6 @@ fun x =>
   | #[] => 0
   | #[3, 4, 5] => 3
   | x => 4 : Array Nat → Nat
-g.match_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) :
-  (x : List α) → ((a : α) → motive [a]) → ((x : List α) → motive x) → motive x
+g.match_1.{u_1, u_2} {α : Type u_1} (motive : List α → Sort u_2) (x✝ : List α) (h_1 : (a : α) → motive [a])
+  (h_2 : (x : List α) → motive x) : motive x✝
 fun e => nomatch e : Empty → False
diff --git a/tests/lean/run/2846.lean b/tests/lean/run/2846.lean
index 88dcf2f153..5bd6aab0f8 100644
--- a/tests/lean/run/2846.lean
+++ b/tests/lean/run/2846.lean
@@ -30,31 +30,41 @@ def Nat.pos_pow_of_pos' {n : Nat} (m : Nat) : 0 < n → 0 < n ^ m := Nat.pos_pow
 
 /-!
 Repetition of a named argument, only the first is printed as a named argument.
+The second is made hygienic.
 -/
 def foo (n n : Nat) : Fin (n + 1) := 0
 
-/-- info: foo (n : Nat) : (n : Nat) → Fin (n + 1) -/
+/-- info: foo (n n✝ : Nat) : Fin (n✝ + 1) -/
 #guard_msgs in #check foo
 
 /-!
-Repetition of a named argument, only the first is printed as a named argument.
-This is checking that shadowing is handled correctly (that's not the responsibility of
-`delabConstWithSignature`, but it assumes that the main delaborator will handle this correctly).
+Same, but a named argument still follows, and its name is preserved.
 -/
+
 def foo' (n n : Nat) (a : Fin ((by clear n; exact n) + 1)) : Fin (n + 1) := 0
 
-/-- info: foo' (n : Nat) : (n_1 : Nat) → Fin (n + 1) → Fin (n_1 + 1) -/
+/-- info: foo' (n n✝ : Nat) (a : Fin (n + 1)) : Fin (n✝ + 1) -/
 #guard_msgs in #check foo'
 
 /-!
-Named argument after inaccessible name, still stays after the colon.
-But, it does not print using named pi notation since this is not a dependent type.
+Named argument after non-dependent inaccessible name, still stays after the colon.
+Prints with named pi notation.
 -/
 def foo'' : String → (needle : String) → String := fun _ yo => yo
 
-/-- info: foo'' : String → String → String -/
+/-- info: foo'' : String → (needle : String) → String -/
 #guard_msgs in #check foo''
 
+/-!
+Named argument after inaccessible name that's still a dependent argument.
+Stays before the colon, and the names are grouped.
+-/
+
+def foo''' : (_ : Nat) → (n : Nat) → Fin (n + by clear n; assumption) := sorry
+
+/-- info: foo''' (x✝ n : Nat) : Fin (n + x✝) -/
+#guard_msgs in #check foo'''
+
 /-!
 Named argument after inaccessible name, still stays after the colon.
 Here, because it's a dependent type the named pi notation shows the name.
diff --git a/tests/lean/run/4320.lean b/tests/lean/run/4320.lean
index b524a9fb0b..adcdfd4a3d 100644
--- a/tests/lean/run/4320.lean
+++ b/tests/lean/run/4320.lean
@@ -8,7 +8,7 @@ def many_map {α β : Type} (f : α → β) : Many α → Many β
 
 /--
 info: many_map.induct {α β : Type} (f : α → β) (motive : Many α → Prop) (case1 : motive Many.none)
-  (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) : ∀ (a : Many α), motive a
+  (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) (a✝ : Many α) : motive a✝
 -/
 #guard_msgs in
 #check many_map.induct
diff --git a/tests/lean/run/5424.lean b/tests/lean/run/5424.lean
index 92a64df01b..cf38cb7833 100644
--- a/tests/lean/run/5424.lean
+++ b/tests/lean/run/5424.lean
@@ -1,3 +1,4 @@
+import Lean
 /-!
 # Long runs of identifiers should include line breaks
 -/
@@ -19,3 +20,12 @@ info: foo
   Nat
 -/
 #guard_msgs(whitespace := exact) in #check foo
+
+/-!
+Issue pointed out by Mario: need spaces between `x✝` and `y✝`.
+-/
+/--
+info: def foo✝ (x✝ y✝ : Nat✝) :=
+  x✝
+-/
+#guard_msgs in #eval do Lean.PrettyPrinter.ppCommand (← `(command| def foo (x y : Nat) := x))
diff --git a/tests/lean/run/974.lean b/tests/lean/run/974.lean
index 395d1918c2..a27878533e 100644
--- a/tests/lean/run/974.lean
+++ b/tests/lean/run/974.lean
@@ -11,24 +11,23 @@ def Formula.count_quantifiers : {n:Nat} → Formula n → Nat
 attribute [simp] Formula.count_quantifiers
 
 /--
-info: Formula.count_quantifiers.eq_1.{u_1} :
-  ∀ (x : Nat) (f₁ f₂ : Formula x), (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers
+info: Formula.count_quantifiers.eq_1.{u_1} (x✝ : Nat) (f₁ f₂ : Formula x✝) :
+  (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_1
 
 /--
-info: Formula.count_quantifiers.eq_2.{u_1} :
-  ∀ (x : Nat) (f : Formula (x + 1)), f.all.count_quantifiers = f.count_quantifiers + 1
+info: Formula.count_quantifiers.eq_2.{u_1} (x✝ : Nat) (f : Formula (x✝ + 1)) :
+  f.all.count_quantifiers = f.count_quantifiers + 1
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_2
 
 /--
-info: Formula.count_quantifiers.eq_3.{u_1} :
-  ∀ (x : Nat) (x_1 : Formula x),
-    (∀ (f₁ f₂ : Formula x), x_1 = f₁.imp f₂ → False) →
-      (∀ (f : Formula (x + 1)), x_1 = f.all → False) → x_1.count_quantifiers = 0
+info: Formula.count_quantifiers.eq_3.{u_1} (x✝ : Nat) (x✝¹ : Formula x✝)
+  (x_4 : ∀ (f₁ f₂ : Formula x✝), x✝¹ = f₁.imp f₂ → False) (x_5 : ∀ (f : Formula (x✝ + 1)), x✝¹ = f.all → False) :
+  x✝¹.count_quantifiers = 0
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_3
diff --git a/tests/lean/run/eqnsPrio.lean b/tests/lean/run/eqnsPrio.lean
index 97613ad6e8..1d33ae6bb9 100644
--- a/tests/lean/run/eqnsPrio.lean
+++ b/tests/lean/run/eqnsPrio.lean
@@ -11,13 +11,13 @@ def foo : Bool → Nat → Nat
   | _, n+1 => foo .false n
 termination_by _ n => n
 
-/-- info: foo.eq_1 : ∀ (x : Bool), foo x 0 = 0 -/
+/-- info: foo.eq_1 (x✝ : Bool) : foo x✝ 0 = 0 -/
 #guard_msgs in
 #check foo.eq_1
 /-- info: foo.eq_2 (n : Nat) : foo true n.succ = foo true n -/
 #guard_msgs in
 #check foo.eq_2
-/-- info: foo.eq_3 : ∀ (x : Bool) (n : Nat), (x = true → False) → foo x n.succ = foo false n -/
+/-- info: foo.eq_3 (x✝ : Bool) (n : Nat) (x_3 : x✝ = true → False) : foo x✝ n.succ = foo false n -/
 #guard_msgs in
 #check foo.eq_3
 
diff --git a/tests/lean/run/funind_demo.lean b/tests/lean/run/funind_demo.lean
index f27d0d4808..deca8f44c6 100644
--- a/tests/lean/run/funind_demo.lean
+++ b/tests/lean/run/funind_demo.lean
@@ -8,8 +8,8 @@ def ackermann : Nat → Nat → Nat
 /--
 info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
   (case2 : ∀ (n : Nat), motive n 1 → motive n.succ 0)
-  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) :
-  ∀ (a a_1 : Nat), motive a a_1
+  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) (a✝ a✝¹ : Nat) :
+  motive a✝ a✝¹
 -/
 #guard_msgs in
 #check ackermann.induct
@@ -19,7 +19,7 @@ def Tree.rev : Tree → Tree | node ts => .node (ts.attach.map (fun ⟨t, _ht⟩
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
-  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a
+  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (a✝ : Tree) : motive a✝
 -/
 #guard_msgs in
 #check Tree.rev.induct
diff --git a/tests/lean/run/funind_fewer_levels.lean b/tests/lean/run/funind_fewer_levels.lean
index 519b4e44bf..453021165d 100644
--- a/tests/lean/run/funind_fewer_levels.lean
+++ b/tests/lean/run/funind_fewer_levels.lean
@@ -10,8 +10,8 @@ def foo.{u} : Nat → PUnit.{u}
 | n+1 => foo n
 
 /--
-info: Structural.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+info: Structural.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
+  (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -31,7 +31,7 @@ termination_by xs => xs
 
 /--
 info: WellFounded.foo.induct.{v} {α : Type v} (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) : ∀ (a : List α), motive a
+  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -58,7 +58,7 @@ end
 
 /--
 info: Mutual.foo.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
-  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a : Nat), motive1 a
+  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (a✝ : Nat) : motive1 a✝
 -/
 #guard_msgs in
 #check foo.induct
diff --git a/tests/lean/run/funind_proof.lean b/tests/lean/run/funind_proof.lean
index bff44bf0e4..f6b24b0c02 100644
--- a/tests/lean/run/funind_proof.lean
+++ b/tests/lean/run/funind_proof.lean
@@ -35,7 +35,7 @@ info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2
   (case1 : ∀ (a_1 : String), (a == a_1) = true → motive1 (const a_1))
   (case2 : ∀ (a_1 : String), ¬(a == a_1) = true → motive1 (const a_1))
   (case3 : ∀ (a : String) (cs : List Term), motive2 cs → motive1 (app a cs)) (case4 : motive2 [])
-  (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) : ∀ (a : Term), motive1 a
+  (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) (a✝ : Term) : motive1 a✝
 -/
 #guard_msgs in
 #check replaceConst.induct
diff --git a/tests/lean/run/funind_structural.lean b/tests/lean/run/funind_structural.lean
index 20b6ce5f56..16b9597626 100644
--- a/tests/lean/run/funind_structural.lean
+++ b/tests/lean/run/funind_structural.lean
@@ -11,7 +11,7 @@ termination_by structural x => x
 
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a : Nat), motive a
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check fib.induct
@@ -24,8 +24,8 @@ termination_by structural x => x
 
 /--
 info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc)
-  (case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc) :
-  ∀ (a a_1 : Nat), motive a a_1
+  (case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc)
+  (a✝ a✝¹ : Nat) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check binary.induct
@@ -40,8 +40,8 @@ termination_by structural _ x => x
 /--
 info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0)
   (case2 : ∀ (acc : Bool), motive acc 1)
-  (case3 : ∀ (acc : Bool) (n : Nat), motive acc (n + 1) → motive (binary' acc (n + 1)) n → motive acc n.succ.succ) :
-  ∀ (a : Bool) (a_1 : Nat), motive a a_1
+  (case3 : ∀ (acc : Bool) (n : Nat), motive acc (n + 1) → motive (binary' acc (n + 1)) n → motive acc n.succ.succ)
+  (a✝ : Bool) (a✝¹ : Nat) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check binary'.induct
@@ -55,8 +55,8 @@ termination_by structural x => x
 /--
 info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
   (case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (t : List α), (t = [] → False) → motive t [])
-  (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) :
-  ∀ (a : List α) (a_1 : List β), motive a a_1
+  (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) (a✝ : List α)
+  (a✝¹ : List β) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check zip.induct
@@ -94,7 +94,7 @@ info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n
   (case1 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), motive x m Finn.fzero x_1)
   (case2 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), (x_1 = Finn.fzero → False) → motive x m x_1 Finn.fzero)
   (case3 : ∀ (x : Bool) (m n : Nat) (i j : Finn n), motive (!x) (m + 1) i j → motive x m i.fsucc j.fsucc) (x : Bool)
-  {n : Nat} (m : Nat) : ∀ (a f : Finn n), motive x m a f
+  {n : Nat} (m : Nat) (a✝ f : Finn n) : motive x m a✝ f
 -/
 #guard_msgs in
 #check Finn.min.induct
@@ -195,7 +195,7 @@ info: TermDenote.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} →
   (case6 :
     ∀ (a : List Ty) (ty ty₁ : Ty) (a_1 : Term a ty₁) (b : Term (ty₁ :: a) ty) (env : HList Ty.denote a),
       motive a_1 env → motive b (HList.cons (a_1.denote env) env) → motive (a_1.let b) env)
-  {ctx : List Ty} {ty : Ty} : ∀ (a : Term ctx ty) (a_1 : HList Ty.denote ctx), motive a a_1
+  {ctx : List Ty} {ty : Ty} (a✝ : Term ctx ty) (a✝¹ : HList Ty.denote ctx) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check TermDenote.Term.denote.induct
diff --git a/tests/lean/run/funind_structural_mutual.lean b/tests/lean/run/funind_structural_mutual.lean
index 399764103c..8f5825658b 100644
--- a/tests/lean/run/funind_structural_mutual.lean
+++ b/tests/lean/run/funind_structural_mutual.lean
@@ -25,8 +25,8 @@ end
 info: Tree.size.induct.{u_1} {α : Type u_1} (motive_1 : Tree α → Prop) (motive_2 : List (Tree α) → Prop)
   (case1 :
     ∀ (a : α) (tsf : Bool → List (Tree α)), motive_2 (tsf true) → motive_2 (tsf false) → motive_1 (Tree.node a tsf))
-  (case2 : motive_2 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_1 t → motive_2 ts → motive_2 (t :: ts)) :
-  ∀ (a : Tree α), motive_1 a
+  (case2 : motive_2 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_1 t → motive_2 ts → motive_2 (t :: ts))
+  (a✝ : Tree α) : motive_1 a✝
 -/
 #guard_msgs in
 #check Tree.size.induct
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 503052b211..d33297ab6b 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -15,8 +15,8 @@ termination_by p => p
 /--
 info: Unary.ackermann.induct (motive : Nat × Nat → Prop) (case1 : ∀ (m : Nat), motive (0, m))
   (case2 : ∀ (n : Nat), motive (n, 1) → motive (n.succ, 0))
-  (case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (n.succ, m.succ)) :
-  ∀ (a : Nat × Nat), motive a
+  (case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (n.succ, m.succ))
+  (a✝ : Nat × Nat) : motive a✝
 -/
 #guard_msgs in
 #check ackermann.induct
@@ -34,8 +34,8 @@ termination_by n m => (n, m)
 /--
 info: Binary.ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
   (case2 : ∀ (n : Nat), motive n 1 → motive n.succ 0)
-  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) :
-  ∀ (a a_1 : Nat), motive a a_1
+  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) (a✝ a✝¹ : Nat) :
+  motive a✝ a✝¹
 -/
 #guard_msgs in
 #check ackermann.induct
@@ -50,7 +50,7 @@ def Tree.rev : Tree → Tree
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
-  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a
+  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) (a✝ : Tree) : motive a✝
 -/
 #guard_msgs in
 #check Tree.rev.induct
@@ -64,7 +64,7 @@ termination_by n => n
 
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a : Nat), motive a
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check fib.induct
@@ -78,8 +78,8 @@ def have_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ) : ∀ (a : Nat), motive a
+info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ)
+  (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check have_tailrec.induct
@@ -94,8 +94,8 @@ def have_non_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
+  (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check have_non_tailrec.induct
@@ -109,8 +109,8 @@ def let_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) (a✝ : Nat) :
+  motive a✝
 -/
 #guard_msgs in
 #check let_tailrec.induct
@@ -125,8 +125,8 @@ def let_non_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
+  (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check let_non_tailrec.induct
@@ -145,7 +145,7 @@ termination_by n => n
 /--
 info: with_ite_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
-  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) : ∀ (a : Nat), motive a
+  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check with_ite_tailrec.induct
@@ -165,7 +165,7 @@ termination_by n => n
 
 /--
 info: with_ite_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive n.succ.succ) : ∀ (a : Nat), motive a
+  (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive n.succ.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check with_ite_non_tailrec.induct
@@ -212,7 +212,7 @@ termination_by n => n
 
 /--
 info: with_match_refining_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 0 → motive (Nat.succ 0))
-  (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) : ∀ (a : Nat), motive a
+  (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check with_match_refining_tailrec.induct
@@ -228,7 +228,7 @@ termination_by i
 /--
 info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (i : Nat), motive i 0)
   (case2 : ∀ (n : Nat), motive 0 n.succ) (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i n.succ)
-  (i : Nat) : ∀ (a : Nat), motive i a
+  (i a✝ : Nat) : motive i a✝
 -/
 #guard_msgs in
 #check with_arg_refining_match1.induct
@@ -260,7 +260,7 @@ termination_by n => n
 /--
 info: with_other_match_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
-  (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive n.succ) : ∀ (a : Nat), motive a
+  (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive n.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check with_other_match_tailrec.induct
@@ -274,8 +274,8 @@ termination_by n => n
 
 /--
 info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (a a_1 x : Nat), motive 0 x a a_1)
-  (case2 : ∀ (a a_1 a_2 x : Nat), motive a_2 x (a % 2) (a_1 % 2) → motive a_2.succ x a a_1) :
-  ∀ (a a_1 a_2 a_3 : Nat), motive a a_1 a_2 a_3
+  (case2 : ∀ (a a_1 a_2 x : Nat), motive a_2 x (a % 2) (a_1 % 2) → motive a_2.succ x a a_1) (a✝ a✝¹ a✝² a✝³ : Nat) :
+  motive a✝ a✝¹ a✝² a✝³
 -/
 #guard_msgs in
 #check with_mixed_match_tailrec.induct
@@ -293,8 +293,8 @@ termination_by n => n
 /--
 info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop)
   (case1 : ∀ (a a_1 a_2 a_3 : Nat), motive 0 a a_1 a_2 a_3) (case2 : ∀ (a a_1 n x : Nat), motive n.succ 0 x a a_1)
-  (case3 : ∀ (a a_1 n a_2 x : Nat), motive n a_2 x (a % 2) (a_1 % 2) → motive n.succ a_2.succ x a a_1) :
-  ∀ (a a_1 a_2 a_3 a_4 : Nat), motive a a_1 a_2 a_3 a_4
+  (case3 : ∀ (a a_1 n a_2 x : Nat), motive n a_2 x (a % 2) (a_1 % 2) → motive n.succ a_2.succ x a a_1)
+  (a✝ a✝¹ a✝² a✝³ a✝⁴ : Nat) : motive a✝ a✝¹ a✝² a✝³ a✝⁴
 -/
 #guard_msgs in
 #check with_mixed_match_tailrec2.induct
@@ -310,8 +310,8 @@ def with_match_non_tailrec : Nat → Nat
 termination_by n => n
 
 /--
-info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
+  (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check with_match_non_tailrec.induct
@@ -333,8 +333,8 @@ info: with_match_non_tailrec_refining.induct (motive : Nat → Prop) (case1 : mo
       (match n with
         | 0 => motive 0
         | m => motive m) →
-        motive n.succ) :
-  ∀ (a : Nat), motive a
+        motive n.succ)
+  (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check with_match_non_tailrec_refining.induct
@@ -350,8 +350,8 @@ termination_by n => n
 
 /--
 info: with_overlap.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) (case3 : motive 2) (case4 : motive 3)
-  (case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+  (case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive n.succ) (a✝ : Nat) :
+  motive a✝
 -/
 #guard_msgs in
 #check with_overlap.induct
@@ -368,7 +368,7 @@ termination_by n => n
 
 /--
 info: UnusedExtraParams.unary.induct (base : Nat) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive n.succ) : ∀ (a : Nat), motive a
+  (case2 : ∀ (n : Nat), motive n → motive n.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check unary.induct
@@ -380,7 +380,7 @@ termination_by n => n
 
 /--
 info: UnusedExtraParams.binary.induct (base : Nat) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-  (case2 : ∀ (n m : Nat), motive n m → motive n.succ m) : ∀ (a a_1 : Nat), motive a a_1
+  (case2 : ∀ (n m : Nat), motive n m → motive n.succ m) (a✝ a✝¹ : Nat) : motive a✝ a✝¹
 -/
 #guard_msgs in
 #check binary.induct
@@ -512,7 +512,7 @@ def foo {α} (x : α) : List α → Nat
 termination_by xs => xs
 /--
 info: LetFun.foo.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
+  (case2 : ∀ (_y : α) (ys : List α), motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -527,7 +527,7 @@ termination_by xs => xs
 
 /--
 info: LetFun.bar.induct.{u_1} {α : Type u_1} (x : α) (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (_y : α) (ys : List α), Nat → motive ys → motive (_y :: ys)) : ∀ (a : List α), motive a
+  (case2 : ∀ (_y : α) (ys : List α), Nat → motive ys → motive (_y :: ys)) (a✝ : List α) : motive a✝
 -/
 #guard_msgs in
 #check bar.induct
@@ -545,7 +545,7 @@ termination_by n => n
 /--
 info: RecCallInDisrs.foo.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), foo n = 0 → motive n → motive n.succ)
-  (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) : ∀ (a : Nat), motive a
+  (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -563,7 +563,7 @@ termination_by n => n
 /--
 info: RecCallInDisrs.bar.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : bar 0 = 0 → motive 0 → motive (Nat.succ 0))
   (case3 : (bar 0 = 0 → False) → motive 0 → motive (Nat.succ 0))
-  (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) : ∀ (a : Nat), motive a
+  (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check bar.induct
@@ -585,14 +585,14 @@ end
 
 /--
 info: EvenOdd.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
-  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a : Nat), motive1 a
+  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (a✝ : Nat) : motive1 a✝
 -/
 #guard_msgs in
 #check even.induct
 
 /--
 info: EvenOdd.odd.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
-  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a : Nat), motive2 a
+  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) (a✝ : Nat) : motive2 a✝
 -/
 #guard_msgs in
 #check odd.induct
@@ -615,7 +615,7 @@ end
 /--
 info: Tree.Tree.map.induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop)
   (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts))
-  (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) : ∀ (a : Tree), motive1 a
+  (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) (a✝ : Tree) : motive1 a✝
 -/
 #guard_msgs in
 #check Tree.map.induct
@@ -686,8 +686,8 @@ info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop) (c
   (case2 : ∀ (k x : Nat), (x = 0 → False) → ∀ (x_2 : Fin k), motive x 0 k x_2)
   (case3 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 0), motive x x_1 0 a)
   (case4 : ∀ (x x_1 : Nat), (x = 0 → False) → (x_1 = 0 → False) → ∀ (a : Fin 1), motive x x_1 1 a)
-  (case5 : ∀ (n m k : Nat) (a : Fin k.succ.succ), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ a) :
-  ∀ (a a_1 k : Nat) (a_2 : Fin k), motive a a_1 k a_2
+  (case5 : ∀ (n m k : Nat) (a : Fin k.succ.succ), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ a)
+  (a✝ a✝¹ k : Nat) (a✝² : Fin k) : motive a✝ a✝¹ k a✝²
 -/
 #guard_msgs in
 #check foo.induct
@@ -739,7 +739,7 @@ termination_by n => n
 /--
 info: PreserveParams.foo.induct (a : Nat) (motive : Nat → Prop) (case1 : motive 0)
   (case2 : ∀ (n : Nat), a = 23 → motive n.succ) (case3 : ¬a = 23 → motive a.succ)
-  (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) : ∀ (a : Nat), motive a
+  (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) (a✝ : Nat) : motive a✝
 -/
 #guard_msgs in
 #check foo.induct
diff --git a/tests/lean/run/namePatEqThm.lean b/tests/lean/run/namePatEqThm.lean
index a618088387..28be818706 100644
--- a/tests/lean/run/namePatEqThm.lean
+++ b/tests/lean/run/namePatEqThm.lean
@@ -26,10 +26,8 @@ info: f.eq_2 (x_1 y : Nat) (zs : List Nat) (x_2 : zs = [] → False) : f (x_1 ::
 #check f.eq_2
 
 /--
-info: f.eq_3 :
-  ∀ (x : List Nat),
-    (∀ (x_1 y : Nat), x = [x_1, y] → False) →
-      (∀ (x_1 y : Nat) (zs : List Nat), x = x_1 :: y :: zs → False) → f x = ([], [])
+info: f.eq_3 (x✝ : List Nat) (x_2 : ∀ (x y : Nat), x✝ = [x, y] → False)
+  (x_3 : ∀ (x y : Nat) (zs : List Nat), x✝ = x :: y :: zs → False) : f x✝ = ([], [])
 -/
 #guard_msgs in
 #check f.eq_3
diff --git a/tests/lean/run/reserved.lean b/tests/lean/run/reserved.lean
index 97540a421c..8b8ba0de93 100644
--- a/tests/lean/run/reserved.lean
+++ b/tests/lean/run/reserved.lean
@@ -40,12 +40,11 @@ def nonrecfun : Bool → Nat
   | true => 0
 
 /--
-info: nonrecfun.eq_def :
-  ∀ (x : Bool),
-    nonrecfun x =
-      match x with
-      | false => 0
-      | true => 0
+info: nonrecfun.eq_def (x✝ : Bool) :
+  nonrecfun x✝ =
+    match x✝ with
+    | false => 0
+    | true => 0
 -/
 #guard_msgs in
 #check nonrecfun.eq_def
@@ -63,12 +62,11 @@ def fact : Nat → Nat
   | n+1 => (n+1) * fact n
 
 /--
-info: fact.eq_def :
-  ∀ (x : Nat),
-    fact x =
-      match x with
-      | 0 => 1
-      | n.succ => (n + 1) * fact n
+info: fact.eq_def (x✝ : Nat) :
+  fact x✝ =
+    match x✝ with
+    | 0 => 1
+    | n.succ => (n + 1) * fact n
 -/
 #guard_msgs in
 #check fact.eq_def
diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean
index 63d7f0a433..cf243b665f 100644
--- a/tests/lean/run/structuralMutual.lean
+++ b/tests/lean/run/structuralMutual.lean
@@ -631,7 +631,7 @@ namespace FunIndTests
 info: A.size.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self)
   (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty)
   (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a))
-  (case6 : motive_2 B.empty) : ∀ (a : A), motive_1 a
+  (case6 : motive_2 B.empty) (a✝ : A) : motive_1 a✝
 -/
 #guard_msgs in
 #check A.size.induct
@@ -649,7 +649,7 @@ info: A.subs.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀
 info: MutualIndNonMutualFun.A.self_size.induct (motive : MutualIndNonMutualFun.A → Prop)
   (case1 : ∀ (a : MutualIndNonMutualFun.A), motive a → motive a.self)
   (case2 : ∀ (a : MutualIndNonMutualFun.B), motive (MutualIndNonMutualFun.A.other a))
-  (case3 : motive MutualIndNonMutualFun.A.empty) : ∀ (a : MutualIndNonMutualFun.A), motive a
+  (case3 : motive MutualIndNonMutualFun.A.empty) (a✝ : MutualIndNonMutualFun.A) : motive a✝
 -/
 #guard_msgs in
 #check MutualIndNonMutualFun.A.self_size.induct
@@ -658,8 +658,8 @@ info: MutualIndNonMutualFun.A.self_size.induct (motive : MutualIndNonMutualFun.A
 info: MutualIndNonMutualFun.A.self_size_with_param.induct (motive : Nat → MutualIndNonMutualFun.A → Prop)
   (case1 : ∀ (n : Nat) (a : MutualIndNonMutualFun.A), motive n a → motive n a.self)
   (case2 : ∀ (x : Nat) (a : MutualIndNonMutualFun.B), motive x (MutualIndNonMutualFun.A.other a))
-  (case3 : ∀ (x : Nat), motive x MutualIndNonMutualFun.A.empty) :
-  ∀ (a : Nat) (a_1 : MutualIndNonMutualFun.A), motive a a_1
+  (case3 : ∀ (x : Nat), motive x MutualIndNonMutualFun.A.empty) (a✝ : Nat) (a✝¹ : MutualIndNonMutualFun.A) :
+  motive a✝ a✝¹
 -/
 #guard_msgs in
 #check MutualIndNonMutualFun.A.self_size_with_param.induct
@@ -668,7 +668,7 @@ info: MutualIndNonMutualFun.A.self_size_with_param.induct (motive : Nat → Mutu
 info: A.hasNoBEmpty.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self)
   (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty)
   (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a))
-  (case6 : motive_2 B.empty) : ∀ (a : A), motive_1 a
+  (case6 : motive_2 B.empty) (a✝ : A) : motive_1 a✝
 -/
 #guard_msgs in
 #check A.hasNoBEmpty.induct
@@ -676,7 +676,7 @@ info: A.hasNoBEmpty.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case
 /--
 info: EvenOdd.isEven.induct (motive_1 motive_2 : Nat → Prop) (case1 : motive_1 0)
   (case2 : ∀ (n : Nat), motive_2 n → motive_1 n.succ) (case3 : motive_2 0)
-  (case4 : ∀ (n : Nat), motive_1 n → motive_2 n.succ) : ∀ (a : Nat), motive_1 a
+  (case4 : ∀ (n : Nat), motive_1 n → motive_2 n.succ) (a✝ : Nat) : motive_1 a✝
 -/
 #guard_msgs in
 #check EvenOdd.isEven.induct
diff --git a/tests/lean/run/unfoldLemma.lean b/tests/lean/run/unfoldLemma.lean
index 01cb1d88a2..ab6f2bd138 100644
--- a/tests/lean/run/unfoldLemma.lean
+++ b/tests/lean/run/unfoldLemma.lean
@@ -12,12 +12,11 @@ theorem Option_map.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α
 #print equations Option_map
 
 /--
-info: Option_map.eq_def.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) :
-  ∀ (x : Option α),
-    Option_map f x =
-      match x with
-      | none => none
-      | some x => some (f x)
+info: Option_map.eq_def.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (x✝ : Option α) :
+  Option_map f x✝ =
+    match x✝ with
+    | none => none
+    | some x => some (f x)
 -/
 #guard_msgs in
 #check Option_map.eq_def
diff --git a/tests/lean/run/wfEqns5.lean b/tests/lean/run/wfEqns5.lean
index 71e48766e6..2e20121a57 100644
--- a/tests/lean/run/wfEqns5.lean
+++ b/tests/lean/run/wfEqns5.lean
@@ -14,15 +14,14 @@ theorem foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
 #print equations foo
 
 /--
-info: foo.eq_def :
-  ∀ (x x_1 : Nat),
-    foo x x_1 =
-      match x, x_1 with
-      | 0, m =>
-        match m with
-        | 0 => 0
-        | m => m
-      | n.succ, m => foo n m
+info: foo.eq_def (x✝ x✝¹ : Nat) :
+  foo x✝ x✝¹ =
+    match x✝, x✝¹ with
+    | 0, m =>
+      match m with
+      | 0 => 0
+      | m => m
+    | n.succ, m => foo n m
 -/
 #guard_msgs in
 #check foo.eq_def
@@ -51,15 +50,14 @@ theorem bar.eq_2 : ∀ (x n : Nat), bar n.succ x = bar n x
 #print equations bar
 
 /--
-info: bar.eq_def :
-  ∀ (x x_1 : Nat),
-    bar x x_1 =
-      match x, x_1 with
-      | 0, m =>
-        match m with
-        | 0 => 0
-        | m => m
-      | n.succ, m => bar n m
+info: bar.eq_def (x✝ x✝¹ : Nat) :
+  bar x✝ x✝¹ =
+    match x✝, x✝¹ with
+    | 0, m =>
+      match m with
+      | 0 => 0
+      | m => m
+    | n.succ, m => bar n m
 -/
 #guard_msgs in
 #check bar.eq_def
@@ -83,15 +81,14 @@ theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
 #print equations foo
 
 /--
-info: Structural.foo.eq_def :
-  ∀ (x x_1 : Nat),
-    foo x x_1 =
-      match x, x_1 with
-      | 0, m =>
-        match m with
-        | 0 => 0
-        | m => m
-      | n.succ, m => foo n m
+info: Structural.foo.eq_def (x✝ x✝¹ : Nat) :
+  foo x✝ x✝¹ =
+    match x✝, x✝¹ with
+    | 0, m =>
+      match m with
+      | 0 => 0
+      | m => m
+    | n.succ, m => foo n m
 -/
 #guard_msgs in
 #check foo.eq_def
@@ -120,15 +117,14 @@ theorem Structural.bar.eq_2 : ∀ (x n : Nat), bar n.succ x = bar n x
 #print equations bar
 
 /--
-info: Structural.bar.eq_def :
-  ∀ (x x_1 : Nat),
-    bar x x_1 =
-      match x, x_1 with
-      | 0, m =>
-        match m with
-        | 0 => 0
-        | m => m
-      | n.succ, m => bar n m
+info: Structural.bar.eq_def (x✝ x✝¹ : Nat) :
+  bar x✝ x✝¹ =
+    match x✝, x✝¹ with
+    | 0, m =>
+      match m with
+      | 0 => 0
+      | m => m
+    | n.succ, m => bar n m
 -/
 #guard_msgs in
 #check bar.eq_def