diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index 5d061fe4c1..c4dcd89e36 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -59,6 +59,14 @@ def ppCommand (stx : Syntax.Command) : CoreM Format := ppCategory `command stx
 def ppModule (stx : TSyntax ``Parser.Module.module) : CoreM Format := do
   parenthesize Lean.Parser.Module.module.parenthesizer stx >>= format Lean.Parser.Module.module.formatter
 
+open Delaborator in
+/-- Pretty-prints a declaration `c` as `c.{<levels>} <params> : <type>`. -/
+def ppSignature (c : Name) : MetaM FormatWithInfos := do
+  let decl ← getConstInfo c
+  let e := .const c (decl.levelParams.map mkLevelParam)
+  let (stx, infos) ← delabCore e (delab := delabConstWithSignature)
+  return ⟨← ppTerm ⟨stx⟩, infos⟩  -- HACK: not a term
+
 private partial def noContext : MessageData → MessageData
   | MessageData.withContext _   msg => noContext msg
   | MessageData.withNamingContext ctx msg => MessageData.withNamingContext ctx (noContext msg)
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 13218f2724..2e1ebeb6ad 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -284,7 +284,9 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delabor
   trace[PrettyPrinter.delab.input] "{Std.format e}"
   let mut opts ← getOptions
   -- default `pp.proofs` to `true` if `e` is a proof
-  if pp.proofs.get? opts == none then
+  if pp.proofs.get? opts == none &&
+      -- necessary for `delabConstWithSignature`, and harmless otherwise
+      !e.isConst then
     try if ← Meta.isProof e then opts := pp.proofs.set opts true
     catch _ => pure ()
   withOptions (fun _ => opts) do
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 4cf71c1fda..0ee5849edd 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -763,4 +763,52 @@ def delabNameMkStr : Delab := whenPPOption getPPNotation do
 @[builtin_delab app.Lean.Name.num]
 def delabNameMkNum : Delab := delabNameMkStr
 
+open Parser Command Term in
+@[run_builtin_parser_attribute_hooks]
+-- use `termParser` instead of `declId` so we can reuse `delabConst`
+def declSigWithId := leading_parser termParser maxPrec >> declSig
+
+private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax :=
+  env.evalConstCheck Syntax opts ``Syntax constName
+
+@[implemented_by evalSyntaxConstantUnsafe]
+private opaque evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw ""
+
+/-- Pretty-prints a constant `c` as `c.{<levels>} <params> : <type>`. -/
+partial def delabConstWithSignature : Delab := do
+  let e ← getExpr
+  -- use virtual expression node of arity 2 to separate name and type info
+  let idStx ← descend e 0 <|
+    withOptions (pp.universes.set · true |> (pp.fullNames.set · true)) <|
+      delabConst
+  descend (← inferType e) 1 <|
+    delabParams idStx #[] #[]
+where
+  -- follows `delabBinders`, but does not uniquify binder names and accumulates all binder groups
+  delabParams (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do
+    if let .forallE n d _ i ← getExpr then
+      let stxN ← annotateCurPos (mkIdent n)
+      let curIds := curIds.push ⟨stxN⟩
+      if ← shouldGroupWithNext then
+        withBindingBody n <| delabParams idStx groups curIds
+      else
+        let delabTy := withOptions (pp.piBinderTypes.set · true) delab
+        let group ← withBindingDomain do
+          match i with
+          | .implicit       => `(bracketedBinderF|{$curIds* : $(← delabTy)})
+          | .strictImplicit => `(bracketedBinderF|⦃$curIds* : $(← delabTy)⦄)
+          | .instImplicit   => `(bracketedBinderF|[$curIds.back : $(← delabTy)])
+          | _ =>
+            if d.isOptParam then
+              `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy)))
+            else if let some (.const tacticDecl _) := d.getAutoParamTactic? then
+              let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl
+              `(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax))
+            else
+              `(bracketedBinderF|($curIds* : $(← delabTy)))
+        withBindingBody n <| delabParams idStx (groups.push group) #[]
+    else
+      let type ← delab
+      `(declSigWithId| $idStx:ident $groups* : $type)
+
 end Lean.PrettyPrinter.Delaborator
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 4fb122a262..c70942cc3a 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -71,7 +71,7 @@ def handleHover (p : HoverParams)
           -- prefer info tree if at least as specific as parser docstring
           if stxDoc?.all fun (_, stxRange) => stxRange.includes range then
             if let some hoverFmt ← i.fmtHover? ci then
-              return mkHover (toString hoverFmt) range
+              return mkHover (toString hoverFmt.fmt) range
 
       if let some (doc, range) := stxDoc? then
         return mkHover doc range
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 3a0e69bb93..b0658aafc0 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -200,13 +200,15 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   return none
 
 /-- Construct a hover popup, if any, from an info node in a context.-/
-def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
+def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option FormatWithInfos) := do
   ci.runMetaM i.lctx do
     let mut fmts := #[]
+    let mut infos := ∅
     let modFmt ← try
       let (termFmt, modFmt) ← fmtTermAndModule?
       if let some f := termFmt then
-        fmts := fmts.push f
+        fmts := fmts.push f.fmt
+        infos := f.infos
       pure modFmt
     catch _ => pure none
     if let some m ← i.docString? then
@@ -216,14 +218,14 @@ def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
     if fmts.isEmpty then
       return none
     else
-      return f!"\n***\n".joinSep fmts.toList
+      return some ⟨f!"\n***\n".joinSep fmts.toList, infos⟩
 
 where
   fmtModule? (decl : Name) : MetaM (Option Format) := do
     let some mod ← findModuleOf? decl | return none
     return some f!"*import {mod}*"
 
-  fmtTermAndModule? : MetaM (Option Format × Option Format) := do
+  fmtTermAndModule? : MetaM (Option FormatWithInfos × Option Format) := do
     match i with
     | Info.ofTermInfo ti =>
       let e ← instantiateMVars ti.expr
@@ -232,20 +234,18 @@ where
         return (none, none)
       let tp ← instantiateMVars (← Meta.inferType e)
       let tpFmt ← Meta.ppExpr tp
-      if e.isConst then
-        -- Recall that `ppExpr` adds a `@` if the constant has implicit arguments, and it is quite distracting
-        let eFmt ← withOptions (pp.fullNames.set · true |> (pp.universes.set · true)) <| PrettyPrinter.ppConst e
-        return (some f!"```lean\n{eFmt} : {tpFmt}\n```", ← fmtModule? e.constName!)
-      else
-        let eFmt ← Meta.ppExpr e
-        -- Try not to show too scary internals
-        let showTerm := if let .fvar _ := e then
-          if let some ldecl := (← getLCtx).findFVar? e then
-            !ldecl.userName.hasMacroScopes
-          else false
-        else isAtomicFormat eFmt
-        let fmt := if showTerm then f!"{eFmt} : {tpFmt}" else tpFmt
-        return (some f!"```lean\n{fmt}\n```", none)
+      if let .const c _ := e then
+        let eFmt ← PrettyPrinter.ppSignature c
+        return (some { eFmt with fmt := f!"```lean\n{eFmt.fmt}\n```" }, ← fmtModule? c)
+      let eFmt ← Meta.ppExpr e
+      -- Try not to show too scary internals
+      let showTerm := if let .fvar _ := e then
+        if let some ldecl := (← getLCtx).findFVar? e then
+          !ldecl.userName.hasMacroScopes
+        else false
+      else isAtomicFormat eFmt
+      let fmt := if showTerm then f!"{eFmt} : {tpFmt}" else tpFmt
+      return (some f!"```lean\n{fmt}\n```", none)
     | Info.ofFieldInfo fi =>
       let tp ← Meta.inferType fi.val
       let tpFmt ← Meta.ppExpr tp
diff --git a/tests/lean/interactive/amb.lean.expected.out b/tests/lean/interactive/amb.lean.expected.out
index 31b6c70a09..d231a2a7ad 100644
--- a/tests/lean/interactive/amb.lean.expected.out
+++ b/tests/lean/interactive/amb.lean.expected.out
@@ -2,10 +2,11 @@
  "position": {"line": 17, "character": 19}}
 {"range":
  {"start": {"line": 17, "character": 19}, "end": {"line": 17, "character": 20}},
- "contents": {"value": "```lean\nFoo.f : Nat → Bool\n```", "kind": "markdown"}}
+ "contents":
+ {"value": "```lean\nFoo.f (n : Nat) : Bool\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://amb.lean"},
  "position": {"line": 19, "character": 19}}
 {"range":
  {"start": {"line": 19, "character": 19}, "end": {"line": 19, "character": 20}},
  "contents":
- {"value": "```lean\nBoo.f : String → String\n```", "kind": "markdown"}}
+ {"value": "```lean\nBoo.f (n : String) : String\n```", "kind": "markdown"}}
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index 5e76ce9f7b..286985ebba 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -256,3 +256,6 @@ example : Nat :=
   let x := match 0 with | _ => 0
   _
 --^ textDocument/hover
+
+def auto (o : Nat := by exact 1) : Nat := o
+  --^ textDocument/hover
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 8ca74f8449..2396a830a7 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -120,7 +120,7 @@
  {"start": {"line": 73, "character": 38}, "end": {"line": 73, "character": 45}},
  "contents":
  {"value":
-  "```lean\nNat.add : Nat → Nat → Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*",
+  "```lean\nNat.add (a✝a✝¹ : Nat) : Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 77, "character": 10}}
@@ -180,7 +180,7 @@
   "end": {"line": 102, "character": 31}},
  "contents":
  {"value":
-  "```lean\nLean.ParserDescr.sepBy1 : Lean.ParserDescr → String → Lean.ParserDescr → optParam Bool false → Lean.ParserDescr\n```\n***\n`sepBy1` is just like `sepBy`, except it takes 1 or more instead of\n0 or more occurrences of `p`. \n***\n*import Init.Prelude*",
+  "```lean\nLean.ParserDescr.sepBy1 (p : Lean.ParserDescr) (sep : String) (psep : Lean.ParserDescr)\n  (allowTrailingSep : Bool := false) : Lean.ParserDescr\n```\n***\n`sepBy1` is just like `sepBy`, except it takes 1 or more instead of\n0 or more occurrences of `p`. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 102, "character": 31}}
@@ -212,7 +212,7 @@
   "end": {"line": 119, "character": 10}},
  "contents":
  {"value":
-  "```lean\nid.{0} : ∀ {α : Prop}, α → α\n```\n***\nThe identity function. `id` takes an implicit argument `α : Sort u`\n(a type in any universe), and an argument `a : α`, and returns `a`.\n\nAlthough this may look like a useless function, one application of the identity\nfunction is to explicitly put a type on an expression. If `e` has type `T`,\nand `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and lean\nknows that this expression has type `T'` rather than `T`. This can make a\ndifference for typeclass inference, since `T` and `T'` may have different\ntypeclass instances on them. `show T' from e` is sugar for an `@id T' e`\nexpression.\n\n***\n*import Init.Prelude*",
+  "```lean\nid.{u} {α : Sort u} (a : α) : α\n```\n***\nThe identity function. `id` takes an implicit argument `α : Sort u`\n(a type in any universe), and an argument `a : α`, and returns `a`.\n\nAlthough this may look like a useless function, one application of the identity\nfunction is to explicitly put a type on an expression. If `e` has type `T`,\nand `T'` is definitionally equal to `T`, then `@id T' e` typechecks, and lean\nknows that this expression has type `T'` rather than `T`. This can make a\ndifference for typeclass inference, since `T` and `T'` may have different\ntypeclass instances on them. `show T' from e` is sugar for an `@id T' e`\nexpression.\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 119, "character": 10}}
@@ -260,13 +260,13 @@
  {"start": {"line": 147, "character": 17},
   "end": {"line": 147, "character": 19}},
  "contents":
- {"value": "```lean\nBar.Foo.mk : ℕ → Foo\n```", "kind": "markdown"}}
+ {"value": "```lean\nBar.Foo.mk (hi : ℕ) : Foo\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 150, "character": 2}}
 {"range":
  {"start": {"line": 150, "character": 2}, "end": {"line": 150, "character": 4}},
  "contents":
- {"value": "```lean\nBar.Foo.hi : Foo → ℕ\n```", "kind": "markdown"}}
+ {"value": "```lean\nBar.Foo.hi (self : Foo) : ℕ\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 153, "character": 10}}
 {"range":
@@ -446,7 +446,7 @@ null
  {"start": {"line": 228, "character": 4}, "end": {"line": 228, "character": 8}},
  "contents":
  {"value":
-  "```lean\nNat.succ : ℕ → ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 228, "character": 9}}
@@ -511,7 +511,7 @@ null
  {"start": {"line": 247, "character": 4}, "end": {"line": 247, "character": 9}},
  "contents":
  {"value":
-  "```lean\nNat.succ : ℕ → ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 247, "character": 17}}
@@ -520,7 +520,7 @@ null
   "end": {"line": 247, "character": 20}},
  "contents":
  {"value":
-  "```lean\nNat.succ : ℕ → ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 250, "character": 27}}
@@ -529,7 +529,7 @@ null
   "end": {"line": 250, "character": 37}},
  "contents":
  {"value":
-  "```lean\nInhabited.mk.{1} : {α : Type} → α → Inhabited α\n```\n***\n*import Init.Prelude*",
+  "```lean\nInhabited.mk.{u} {α : Sort u} (default : α) : Inhabited α\n```\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 250, "character": 28}}
@@ -548,3 +548,10 @@ null
  {"value":
   "```lean\nlet x :=\n  match 0 with\n  | x => 0;\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ",
   "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 259, "character": 4}}
+{"range":
+ {"start": {"line": 259, "character": 4}, "end": {"line": 259, "character": 8}},
+ "contents":
+ {"value": "```lean\nBar.auto (o : ℕ := by exact 1) : ℕ\n```",
+  "kind": "markdown"}}
diff --git a/tests/lean/interactive/hoverAt.lean.expected.out b/tests/lean/interactive/hoverAt.lean.expected.out
index 3aaa8144aa..3634be3173 100644
--- a/tests/lean/interactive/hoverAt.lean.expected.out
+++ b/tests/lean/interactive/hoverAt.lean.expected.out
@@ -4,5 +4,5 @@
  {"start": {"line": 8, "character": 17}, "end": {"line": 8, "character": 34}},
  "contents":
  {"value":
-  "```lean\nPalindrome.single.{u_1} : ∀ {α : Type u_1} (a : α), Palindrome [a]\n```",
+  "```lean\nPalindrome.single.{u_1} {α : Type u_1} (a : α) : Palindrome [a]\n```",
   "kind": "markdown"}}
diff --git a/tests/lean/interactive/hoverDot.lean.expected.out b/tests/lean/interactive/hoverDot.lean.expected.out
index b7b8d13761..09f0cb0da5 100644
--- a/tests/lean/interactive/hoverDot.lean.expected.out
+++ b/tests/lean/interactive/hoverDot.lean.expected.out
@@ -12,51 +12,55 @@
  "position": {"line": 12, "character": 11}}
 {"range":
  {"start": {"line": 12, "character": 11}, "end": {"line": 12, "character": 13}},
- "contents": {"value": "```lean\nFoo.f₁ : Foo → Nat\n```", "kind": "markdown"}}
+ "contents":
+ {"value": "```lean\nFoo.f₁ (self : Foo) : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 12, "character": 14}}
 {"range":
  {"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 18}},
  "contents":
  {"value":
-  "```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 16, "character": 11}}
 {"range":
  {"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 13}},
- "contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}}
+ "contents":
+ {"value": "```lean\nFoo.f₂ (f : Foo) : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 16, "character": 14}}
 {"range":
  {"start": {"line": 16, "character": 14}, "end": {"line": 16, "character": 18}},
  "contents":
  {"value":
-  "```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 19, "character": 13}}
 {"range":
  {"start": {"line": 19, "character": 13}, "end": {"line": 19, "character": 15}},
- "contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}}
+ "contents":
+ {"value": "```lean\nFoo.f₂ (f : Foo) : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 19, "character": 16}}
 {"range":
  {"start": {"line": 19, "character": 16}, "end": {"line": 19, "character": 20}},
  "contents":
  {"value":
-  "```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 22, "character": 14}}
 {"range":
  {"start": {"line": 22, "character": 14}, "end": {"line": 22, "character": 16}},
- "contents": {"value": "```lean\nFoo.f₂ : Foo → Nat\n```", "kind": "markdown"}}
+ "contents":
+ {"value": "```lean\nFoo.f₂ (f : Foo) : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 22, "character": 17}}
 {"range":
  {"start": {"line": 22, "character": 17}, "end": {"line": 22, "character": 21}},
  "contents":
  {"value":
-  "```lean\nNat.succ : Nat → Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
+  "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
diff --git a/tests/lean/interactive/lean3HoverIssue.lean.expected.out b/tests/lean/interactive/lean3HoverIssue.lean.expected.out
index 8d10618c6b..69490e2141 100644
--- a/tests/lean/interactive/lean3HoverIssue.lean.expected.out
+++ b/tests/lean/interactive/lean3HoverIssue.lean.expected.out
@@ -4,7 +4,7 @@
  {"start": {"line": 0, "character": 54}, "end": {"line": 0, "character": 58}},
  "contents":
  {"value":
-  "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
+  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://lean3HoverIssue.lean"},
  "position": {"line": 0, "character": 52}}
@@ -17,7 +17,7 @@
  {"start": {"line": 4, "character": 45}, "end": {"line": 4, "character": 49}},
  "contents":
  {"value":
-  "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
+  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://lean3HoverIssue.lean"},
  "position": {"line": 7, "character": 54}}
@@ -25,7 +25,7 @@
  {"start": {"line": 7, "character": 53}, "end": {"line": 7, "character": 60}},
  "contents":
  {"value":
-  "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
+  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://lean3HoverIssue.lean"},
  "position": {"line": 7, "character": 65}}
@@ -33,7 +33,7 @@
  {"start": {"line": 7, "character": 62}, "end": {"line": 7, "character": 69}},
  "contents":
  {"value":
-  "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
+  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://lean3HoverIssue.lean"},
  "position": {"line": 7, "character": 70}}
@@ -46,5 +46,5 @@
  {"start": {"line": 7, "character": 72}, "end": {"line": 7, "character": 76}},
  "contents":
  {"value":
-  "```lean\nEq.symm.{1} : ∀ {α : Type} {a b : α}, a = b → b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
+  "```lean\nEq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a\n```\n***\nEquality is symmetric: if `a = b` then `b = a`.\n\nBecause this is in the `Eq` namespace, if you have a variable `h : a = b`,\n`h.symm` can be used as shorthand for `Eq.symm h` as a proof of `b = a`.\n\nFor more information: [Equality](https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)\n\n***\n*import Init.Prelude*",
   "kind": "markdown"}}