diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index 62ab7fdcf9..36a40ec76b 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -43,3 +43,4 @@ import Lean.Elab.BuiltinCommand
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.Eval
 import Lean.Elab.Calc
+import Lean.Elab.InheritDoc
diff --git a/src/Lean/Elab/InheritDoc.lean b/src/Lean/Elab/InheritDoc.lean
new file mode 100644
index 0000000000..61393813e3
--- /dev/null
+++ b/src/Lean/Elab/InheritDoc.lean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Elab.InfoTree.Main
+import Lean.DocString
+
+namespace Lean
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name := `inheritDoc
+    descr := "inherit documentation from a specified declaration"
+    add   := fun decl stx kind => do
+      unless kind == AttributeKind.global do
+        throwError "invalid `[inheritDoc]` attribute, must be global"
+      match stx with
+      | `(attr| inheritDoc $[$id?:ident]?) =>
+        let some id := id?
+          | throwError "invalid `[inheritDoc]` attribute, could not infer doc source"
+        let declName ← Elab.resolveGlobalConstNoOverloadWithInfo id
+        if (← findDocString? (← getEnv) decl).isSome then
+          logWarningAt id m!"{← mkConstWithLevelParams decl} already has a doc string"
+        let some doc ← findDocString? (← getEnv) declName
+          | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string"
+        addDocString decl doc
+      | _  => throwError "invalid `[inheritDoc]` attribute"
+  }
diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean
index 113f2d0c55..93c58e63ae 100644
--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -24,6 +24,18 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
     | Syntax.node i k args => Syntax.node i k (args.map (antiquote vars))
     | stx => stx
 
+ def addInheritDocDefault (rhs : Term) (attrs? : Option (TSepArray ``attrInstance ",")) :
+    Option (TSepArray ``attrInstance ",") :=
+  attrs?.map fun attrs =>
+    match rhs with
+    | `($f:ident $_args*) =>
+      attrs.getElems.map fun stx => Unhygienic.run do
+        if let `(attrInstance| $attr:ident) := stx then
+          if attr.getId.eraseMacroScopes == `inheritDoc then
+            return ← `(attrInstance| $attr:ident $f:ident)
+        pure ⟨stx⟩
+    | _ => attrs
+
 /-- Convert `notation` command lhs item into a `syntax` command item -/
 def expandNotationItemIntoSyntaxItem : TSyntax ``notationItem → MacroM (TSyntax `stx)
   | `(notationItem| $_:ident$[:$prec?]?) => `(stx| term $[:$prec?]?)
@@ -124,6 +136,7 @@ private def expandNotationAux (ref : Syntax) (currNamespace : Name)
   let vars := items.filter fun item => item.raw.getKind == ``identPrec
   let vars := vars.map fun var => var.raw[0]
   let qrhs := ⟨antiquote vars rhs⟩
+  let attrs? := addInheritDocDefault rhs attrs?
   let patArgs ← items.mapM expandNotationItemIntoPattern
   /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
      So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean
index c5afc3b6ae..d730820e6b 100644
--- a/src/Lean/Linter/MissingDocs.lean
+++ b/src/Lean/Linter/MissingDocs.lean
@@ -110,6 +110,14 @@ def lintField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
 def lintStructField (parent stx : Syntax) (msg : String) : CommandElabM Unit :=
   lint stx s!"{msg} {parent.getId}.{stx.getId}"
 
+def hasInheritDoc (attrs : Syntax) : Bool :=
+  attrs[0][1].getSepArgs.any fun attr =>
+    attr[1].isOfKind ``Parser.Attr.simple &&
+    attr[1][0].getId.eraseMacroScopes == `inheritDoc
+
+def declModifiersPubNoDoc (mods : Syntax) : Bool :=
+  mods[2][0].getKind != ``«private» && mods[0].isNone && !hasInheritDoc mods[1]
+
 def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do
   if k == ``«abbrev» then lintNamed id "public abbrev"
   else if k == ``«def» then lintNamed id "public def"
@@ -124,21 +132,20 @@ def checkDecl : SimpleHandler := fun stx => do
   let head := stx[0]; let rest := stx[1]
   if head[2][0].getKind == ``«private» then return -- not private
   let k := rest.getKind
-  if head[0].isNone then -- no doc string
+  if declModifiersPubNoDoc head then -- no doc string
     lintDeclHead k rest[1][0]
   if k == ``«inductive» || k == ``classInductive then
     for stx in rest[4].getArgs do
       let head := stx[1]
-      if head[2][0].getKind != ``«private» && head[0].isNone then
+      if declModifiersPubNoDoc head then
         lintField rest[1][0] stx[2] "public constructor"
     unless rest[5].isNone do
       for stx in rest[5][0][1].getArgs do
         let head := stx[0]
-        if head[2][0].getKind == ``«private» then return -- not private
-        if head[0].isNone then -- no doc string
+        if declModifiersPubNoDoc head then -- no doc string
           lintField rest[1][0] stx[1] "computed field"
   else if rest.getKind == ``«structure» then
-    unless rest[5].isNone || rest[5][2].isNone do
+    unless rest[5][2].isNone do
       let redecls : Std.HashSet String.Pos :=
         (← get).infoState.trees.foldl (init := {}) fun s tree =>
           tree.foldInfo (init := s) fun _ info s =>
@@ -154,7 +161,7 @@ def checkDecl : SimpleHandler := fun stx => do
         lintField parent stx "public field"
       for stx in rest[5][2][0].getArgs do
         let head := stx[0]
-        if head[2][0].getKind != ``«private» && head[0].isNone then
+        if declModifiersPubNoDoc head then
           if stx.getKind == ``structSimpleBinder then
             lint1 stx[1]
           else
@@ -163,25 +170,24 @@ def checkDecl : SimpleHandler := fun stx => do
 
 @[builtinMissingDocsHandler «initialize»]
 def checkInit : SimpleHandler := fun stx => do
-  if stx[2].isNone then return
-  if stx[0][2][0].getKind != ``«private» && stx[0][0].isNone then
+  if !stx[2].isNone && declModifiersPubNoDoc stx[0] then
     lintNamed stx[2][0] "initializer"
 
 @[builtinMissingDocsHandler «notation»]
 def checkNotation : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
     if stx[5].isNone then lint stx[3] "notation"
     else lintNamed stx[5][0][3] "notation"
 
 @[builtinMissingDocsHandler «mixfix»]
 def checkMixfix : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
     if stx[5].isNone then lint stx[3] stx[3][0].getAtomVal!
     else lintNamed stx[5][0][3] stx[3][0].getAtomVal!
 
 @[builtinMissingDocsHandler «syntax»]
 def checkSyntax : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
     if stx[5].isNone then lint stx[3] "syntax"
     else lintNamed stx[5][0][3] "syntax"
 
@@ -197,20 +203,19 @@ def checkSyntaxCat : SimpleHandler := mkSimpleHandler "syntax category"
 
 @[builtinMissingDocsHandler «macro»]
 def checkMacro : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
     if stx[5].isNone then lint stx[3] "macro"
     else lintNamed stx[5][0][3] "macro"
 
 @[builtinMissingDocsHandler «elab»]
 def checkElab : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
     if stx[5].isNone then lint stx[3] "elab"
     else lintNamed stx[5][0][3] "elab"
 
 @[builtinMissingDocsHandler classAbbrev]
 def checkClassAbbrev : SimpleHandler := fun stx => do
-  let head := stx[0]
-  if head[2][0].getKind != ``«private» && head[0].isNone then
+  if declModifiersPubNoDoc stx[0] then
     lintNamed stx[3] "class abbrev"
 
 @[builtinMissingDocsHandler Parser.Tactic.declareSimpLikeTactic]
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index cc42cc1db8..7d6bd283b9 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -69,8 +69,10 @@ elab_rules : term
 #check mynota' 1
      --^ textDocument/hover
 
-infix:65 " >+< " => Nat.add
+@[inheritDoc]
+infix:65 (name := myInfix) " >+< " => Nat.add
                    --^ textDocument/hover
+                                     --^ textDocument/hover
 
 #check 1 >+< 2
         --^ textDocument/hover
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 5d72233fac..58bc386d73 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -101,248 +101,254 @@
  "contents":
  {"value": "```lean\nNat\n```\n***\nMy ultimate notation ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 71, "character": 21}}
+ "position": {"line": 72, "character": 21}}
+null
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 72, "character": 39}}
 {"range":
- {"start": {"line": 71, "character": 20}, "end": {"line": 71, "character": 27}},
+ {"start": {"line": 72, "character": 38}, "end": {"line": 72, "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",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 74, "character": 10}}
+ "position": {"line": 76, "character": 10}}
 {"range":
- {"start": {"line": 74, "character": 7}, "end": {"line": 74, "character": 14}},
- "contents": {"value": "```lean\nNat\n```", "kind": "markdown"}}
+ {"start": {"line": 76, "character": 7}, "end": {"line": 76, "character": 14}},
+ "contents":
+ {"value":
+  "```lean\nNat\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",
+  "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 79, "character": 14}}
+ "position": {"line": 81, "character": 14}}
 {"range":
- {"start": {"line": 79, "character": 14}, "end": {"line": 79, "character": 36}},
+ {"start": {"line": 81, "character": 14}, "end": {"line": 81, "character": 36}},
  "contents":
  {"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 81, "character": 30}}
+ "position": {"line": 83, "character": 30}}
 {"range":
- {"start": {"line": 81, "character": 29}, "end": {"line": 81, "character": 34}},
+ {"start": {"line": 83, "character": 29}, "end": {"line": 83, "character": 34}},
  "contents":
  {"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 84, "character": 2}}
+ "position": {"line": 86, "character": 2}}
 {"range":
- {"start": {"line": 84, "character": 0}, "end": {"line": 84, "character": 7}},
+ {"start": {"line": 86, "character": 0}, "end": {"line": 86, "character": 7}},
  "contents": {"value": "My command ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 91, "character": 2}}
+ "position": {"line": 93, "character": 2}}
 {"range":
- {"start": {"line": 91, "character": 0}, "end": {"line": 91, "character": 7}},
+ {"start": {"line": 93, "character": 0}, "end": {"line": 93, "character": 7}},
  "contents": {"value": "My command ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 94, "character": 16}}
+ "position": {"line": 96, "character": 16}}
 {"range":
- {"start": {"line": 94, "character": 16}, "end": {"line": 94, "character": 23}},
+ {"start": {"line": 96, "character": 16}, "end": {"line": 96, "character": 23}},
  "contents":
  {"value":
   "```lean\nLean.Parser.ppSpace : Lean.Parser.Parser\n```\n***\nNo-op parser that advises the pretty printer to emit a space/soft line break. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 94, "character": 24}}
+ "position": {"line": 96, "character": 24}}
 {"range":
- {"start": {"line": 94, "character": 24}, "end": {"line": 94, "character": 31}},
+ {"start": {"line": 96, "character": 24}, "end": {"line": 96, "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`. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 94, "character": 31}}
+ "position": {"line": 96, "character": 31}}
 {"range":
- {"start": {"line": 94, "character": 31}, "end": {"line": 94, "character": 35}},
+ {"start": {"line": 96, "character": 31}, "end": {"line": 96, "character": 35}},
  "contents":
  {"value":
   "```lean\nLean.Parser.Category.term : Lean.Parser.Category\n```\n***\n`term` is the builtin syntax category for terms. A term denotes an expression\nin lean's type theory, for example `2 + 2` is a term. The difference between\n`Term` and `Expr` is that the former is a kind of syntax, while the latter is\nthe result of elaboration. For example `by simp` is also a `Term`, but it elaborates\nto different `Expr`s depending on the context. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 103, "character": 2}}
+ "position": {"line": 105, "character": 2}}
 {"range":
- {"start": {"line": 103, "character": 0}, "end": {"line": 103, "character": 8}},
+ {"start": {"line": 105, "character": 0}, "end": {"line": 105, "character": 8}},
  "contents": {"value": "My ultimate command ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 107, "character": 10}}
+ "position": {"line": 109, "character": 10}}
 null
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 111, "character": 8}}
+ "position": {"line": 113, "character": 8}}
 {"range":
- {"start": {"line": 111, "character": 8},
-  "end": {"line": 111, "character": 10}},
+ {"start": {"line": 113, "character": 8},
+  "end": {"line": 113, "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",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 111, "character": 10}}
+ "position": {"line": 113, "character": 10}}
 {"range":
- {"start": {"line": 111, "character": 8},
-  "end": {"line": 111, "character": 21}},
+ {"start": {"line": 113, "character": 8},
+  "end": {"line": 113, "character": 21}},
  "contents": {"value": "```lean\nTrue\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 118, "character": 2}}
+ "position": {"line": 120, "character": 2}}
 {"range":
- {"start": {"line": 118, "character": 2}, "end": {"line": 118, "character": 3}},
+ {"start": {"line": 120, "character": 2}, "end": {"line": 120, "character": 3}},
  "contents": {"value": "```lean\nn : Id Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 125, "character": 9}}
+ "position": {"line": 127, "character": 9}}
 {"range":
- {"start": {"line": 125, "character": 7},
-  "end": {"line": 125, "character": 17}},
+ {"start": {"line": 127, "character": 7},
+  "end": {"line": 127, "character": 17}},
  "contents": {"value": "```lean\nfoo : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 130, "character": 7}}
+ "position": {"line": 132, "character": 7}}
 {"range":
- {"start": {"line": 130, "character": 7},
-  "end": {"line": 130, "character": 10}},
+ {"start": {"line": 132, "character": 7},
+  "end": {"line": 132, "character": 10}},
  "contents": {"value": "```lean\nBar.foo : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 133, "character": 9}}
+ "position": {"line": 135, "character": 9}}
 {"range":
- {"start": {"line": 133, "character": 7},
-  "end": {"line": 133, "character": 17}},
+ {"start": {"line": 135, "character": 7},
+  "end": {"line": 135, "character": 17}},
  "contents": {"value": "```lean\n_root_.foo : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 136, "character": 4}}
+ "position": {"line": 138, "character": 4}}
 {"range":
- {"start": {"line": 136, "character": 4}, "end": {"line": 136, "character": 7}},
+ {"start": {"line": 138, "character": 4}, "end": {"line": 138, "character": 7}},
  "contents": {"value": "```lean\nBar.bar : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 139, "character": 10}}
+ "position": {"line": 141, "character": 10}}
 {"range":
- {"start": {"line": 139, "character": 10},
-  "end": {"line": 139, "character": 13}},
+ {"start": {"line": 141, "character": 10},
+  "end": {"line": 141, "character": 13}},
  "contents": {"value": "```lean\nBar.Foo : Type\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 139, "character": 17}}
+ "position": {"line": 141, "character": 17}}
 {"range":
- {"start": {"line": 139, "character": 17},
-  "end": {"line": 139, "character": 19}},
+ {"start": {"line": 141, "character": 17},
+  "end": {"line": 141, "character": 19}},
  "contents":
  {"value": "```lean\nBar.Foo.mk : Nat → Foo\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 142, "character": 2}}
+ "position": {"line": 144, "character": 2}}
 {"range":
- {"start": {"line": 142, "character": 2}, "end": {"line": 142, "character": 4}},
+ {"start": {"line": 144, "character": 2}, "end": {"line": 144, "character": 4}},
  "contents":
  {"value": "```lean\nBar.Foo.hi : Foo → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 145, "character": 10}}
+ "position": {"line": 147, "character": 10}}
 {"range":
- {"start": {"line": 145, "character": 10},
-  "end": {"line": 145, "character": 13}},
+ {"start": {"line": 147, "character": 10},
+  "end": {"line": 147, "character": 13}},
  "contents": {"value": "```lean\nBar.Bar : Type\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 147, "character": 4}}
+ "position": {"line": 149, "character": 4}}
 {"range":
- {"start": {"line": 147, "character": 4}, "end": {"line": 147, "character": 6}},
+ {"start": {"line": 149, "character": 4}, "end": {"line": 149, "character": 6}},
  "contents": {"value": "```lean\nBar.Bar.mk : Bar\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 150, "character": 2}}
+ "position": {"line": 152, "character": 2}}
 {"range":
- {"start": {"line": 150, "character": 0}, "end": {"line": 150, "character": 8}},
+ {"start": {"line": 152, "character": 0}, "end": {"line": 152, "character": 8}},
  "contents":
  {"value": "```lean\nBar.instToStringNat : ToString Nat\n```",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 152, "character": 9}}
+ "position": {"line": 154, "character": 9}}
 {"range":
- {"start": {"line": 152, "character": 9},
-  "end": {"line": 152, "character": 10}},
+ {"start": {"line": 154, "character": 9},
+  "end": {"line": 154, "character": 10}},
  "contents":
  {"value": "```lean\nBar.f : ToString Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 155, "character": 10}}
+ "position": {"line": 157, "character": 10}}
 {"range":
- {"start": {"line": 155, "character": 10},
-  "end": {"line": 155, "character": 16}},
+ {"start": {"line": 157, "character": 10},
+  "end": {"line": 157, "character": 16}},
  "contents":
  {"value": "A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 158, "character": 4}}
+ "position": {"line": 160, "character": 4}}
 {"range":
- {"start": {"line": 158, "character": 4},
-  "end": {"line": 158, "character": 11}},
+ {"start": {"line": 160, "character": 4},
+  "end": {"line": 160, "character": 11}},
  "contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 158, "character": 8}}
+ "position": {"line": 160, "character": 8}}
 {"range":
- {"start": {"line": 158, "character": 4},
-  "end": {"line": 158, "character": 11}},
+ {"start": {"line": 160, "character": 4},
+  "end": {"line": 160, "character": 11}},
  "contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 163, "character": 6}}
+ "position": {"line": 165, "character": 6}}
 {"range":
- {"start": {"line": 163, "character": 6}, "end": {"line": 163, "character": 7}},
+ {"start": {"line": 165, "character": 6}, "end": {"line": 165, "character": 7}},
  "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 166, "character": 4}}
+ "position": {"line": 168, "character": 4}}
 [{"targetUri": "file://hover.lean",
   "targetSelectionRange":
-  {"start": {"line": 163, "character": 6},
-   "end": {"line": 163, "character": 7}},
+  {"start": {"line": 165, "character": 6},
+   "end": {"line": 165, "character": 7}},
   "targetRange":
-  {"start": {"line": 163, "character": 6},
-   "end": {"line": 163, "character": 7}},
+  {"start": {"line": 165, "character": 6},
+   "end": {"line": 165, "character": 7}},
   "originSelectionRange":
-  {"start": {"line": 166, "character": 4},
-   "end": {"line": 166, "character": 5}}}]
+  {"start": {"line": 168, "character": 4},
+   "end": {"line": 168, "character": 5}}}]
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 166, "character": 4}}
+ "position": {"line": 168, "character": 4}}
 {"range":
- {"start": {"line": 166, "character": 4}, "end": {"line": 166, "character": 5}},
+ {"start": {"line": 168, "character": 4}, "end": {"line": 168, "character": 5}},
  "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 170, "character": 8}}
+ "position": {"line": 172, "character": 8}}
 {"range":
- {"start": {"line": 170, "character": 8}, "end": {"line": 170, "character": 9}},
+ {"start": {"line": 172, "character": 8}, "end": {"line": 172, "character": 9}},
  "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 173, "character": 8}}
+ "position": {"line": 175, "character": 8}}
 [{"targetUri": "file://hover.lean",
   "targetSelectionRange":
-  {"start": {"line": 170, "character": 8},
-   "end": {"line": 170, "character": 9}},
+  {"start": {"line": 172, "character": 8},
+   "end": {"line": 172, "character": 9}},
   "targetRange":
-  {"start": {"line": 170, "character": 8},
-   "end": {"line": 170, "character": 9}},
+  {"start": {"line": 172, "character": 8},
+   "end": {"line": 172, "character": 9}},
   "originSelectionRange":
-  {"start": {"line": 173, "character": 8},
-   "end": {"line": 173, "character": 9}}}]
+  {"start": {"line": 175, "character": 8},
+   "end": {"line": 175, "character": 9}}}]
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 173, "character": 8}}
+ "position": {"line": 175, "character": 8}}
 {"range":
- {"start": {"line": 173, "character": 8}, "end": {"line": 173, "character": 9}},
+ {"start": {"line": 175, "character": 8}, "end": {"line": 175, "character": 9}},
  "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 178, "character": 25}}
+ "position": {"line": 180, "character": 25}}
 {"range":
- {"start": {"line": 178, "character": 25},
-  "end": {"line": 178, "character": 26}},
+ {"start": {"line": 180, "character": 25},
+  "end": {"line": 180, "character": 26}},
  "contents": {"value": "```lean\nn : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 181, "character": 2}}
+ "position": {"line": 183, "character": 2}}
 null
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 187, "character": 2}}
+ "position": {"line": 189, "character": 2}}
 {"range":
- {"start": {"line": 187, "character": 2},
-  "end": {"line": 187, "character": 15}},
+ {"start": {"line": 189, "character": 2},
+  "end": {"line": 189, "character": 15}},
  "contents":
  {"value":
   "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 190, "character": 28}}
+ "position": {"line": 192, "character": 28}}
 {"range":
- {"start": {"line": 190, "character": 27},
-  "end": {"line": 190, "character": 32}},
+ {"start": {"line": 192, "character": 27},
+  "end": {"line": 192, "character": 32}},
  "contents":
  {"value":
   "```lean\nId Nat\n```\n***\nYou can use parentheses for\n- Grouping expressions, e.g., `a * (b + c)`.\n- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.\n- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.\n- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.\n- Creating simple functions when combined with `·`. Here are some examples:\n  - `(· + 1)` is shorthand for `fun x => x + 1`\n  - `(· + ·)` is shorthand for `fun x y => x + y`\n  - `(f · a b)` is shorthand for `fun x => f x a b`\n  - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`\n",