diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index 194d776643..35f465a722 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -234,23 +234,44 @@ def pushInfoLeaf (t : Info) : m Unit := do
 def addCompletionInfo (info : CompletionInfo) : m Unit := do
   pushInfoLeaf <| Info.ofCompletionInfo info
 
-/-- This does the same job as resolveGlobalConstNoOverload; resolving an identifier
+def addConstInfo [MonadEnv m] [MonadError m]
+    (stx : Syntax) (n : Name) (expectedType? : Option Expr := none) : m Unit := do
+  pushInfoLeaf <| .ofTermInfo {
+    elaborator := .anonymous
+    lctx := .empty
+    expr := (← mkConstWithLevelParams n)
+    stx
+    expectedType?
+  }
+
+/-- This does the same job as `resolveGlobalConstNoOverload`; resolving an identifier
 syntax to a unique fully resolved name or throwing if there are ambiguities.
 But also adds this resolved name to the infotree. This means that when you hover
 over a name in the sourcefile you will see the fully resolved name in the hover info.-/
-def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) (expectedType? : Option Expr := none) : m Name := do
+def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m]
+    (id : Syntax) (expectedType? : Option Expr := none) : m Name := do
   let n ← resolveGlobalConstNoOverload id
   if (← getInfoState).enabled then
     -- we do not store a specific elaborator since identifiers are special-cased by the server anyway
-    pushInfoLeaf <| Info.ofTermInfo { elaborator := Name.anonymous, lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := id, expectedType? }
+    addConstInfo id n expectedType?
   return n
 
-/-- Similar to resolveGlobalConstNoOverloadWithInfo, except if there are multiple name resolutions then it returns them as a list. -/
-def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) (expectedType? : Option Expr := none) : m (List Name) := do
+/-- Similar to `resolveGlobalConstNoOverloadWithInfo`, except if there are multiple name resolutions then it returns them as a list. -/
+def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
+    (id : Syntax) (expectedType? : Option Expr := none) : m (List Name) := do
   let ns ← resolveGlobalConst id
   if (← getInfoState).enabled then
     for n in ns do
-      pushInfoLeaf <| Info.ofTermInfo { elaborator := Name.anonymous, lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := id, expectedType? }
+      addConstInfo id n expectedType?
+  return ns
+
+/-- Similar to `resolveGlobalName`, but it also adds the resolved name to the info tree. -/
+def resolveGlobalNameWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m]
+    (ref : Syntax) (id : Name) : m (List (Name × List String)) := do
+  let ns ← resolveGlobalName id
+  if (← getInfoState).enabled then
+    for (n, _) in ns do
+      addConstInfo ref n
   return ns
 
 /-- Use this to descend a node on the infotree that is being built.
diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean
index f0ac3bd9d6..3e44fc9061 100644
--- a/src/Lean/Elab/Quotation/Precheck.lean
+++ b/src/Lean/Elab/Quotation/Precheck.lean
@@ -92,7 +92,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
        notation "x++" => x.foo
        ```
     -/
-    if let _::_ ← resolveGlobalName val then
+    if let _::_ ← resolveGlobalNameWithInfos stx val then
       return
     if (← read).quotLCtx.contains val then
       return
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index 030ca2758d..cc42cc1db8 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -69,6 +69,11 @@ elab_rules : term
 #check mynota' 1
      --^ textDocument/hover
 
+infix:65 " >+< " => Nat.add
+                   --^ textDocument/hover
+
+#check 1 >+< 2
+        --^ textDocument/hover
 
 /-- My command -/
 macro "mycmd" e:term : command => do
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 1f18a01d81..5d72233fac 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -101,235 +101,248 @@
  "contents":
  {"value": "```lean\nNat\n```\n***\nMy ultimate notation ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 74, "character": 14}}
+ "position": {"line": 71, "character": 21}}
 {"range":
- {"start": {"line": 74, "character": 14}, "end": {"line": 74, "character": 36}},
+ {"start": {"line": 71, "character": 20}, "end": {"line": 71, "character": 27}},
+ "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}}
+{"range":
+ {"start": {"line": 74, "character": 7}, "end": {"line": 74, "character": 14}},
+ "contents": {"value": "```lean\nNat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 79, "character": 14}}
+{"range":
+ {"start": {"line": 79, "character": 14}, "end": {"line": 79, "character": 36}},
  "contents":
  {"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 76, "character": 30}}
+ "position": {"line": 81, "character": 30}}
 {"range":
- {"start": {"line": 76, "character": 29}, "end": {"line": 76, "character": 34}},
+ {"start": {"line": 81, "character": 29}, "end": {"line": 81, "character": 34}},
  "contents":
  {"value": "```lean\nLean.Parser.Term.doSeq : Lean.Parser.Parser\n```",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 79, "character": 2}}
+ "position": {"line": 84, "character": 2}}
 {"range":
- {"start": {"line": 79, "character": 0}, "end": {"line": 79, "character": 7}},
+ {"start": {"line": 84, "character": 0}, "end": {"line": 84, "character": 7}},
  "contents": {"value": "My command ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 86, "character": 2}}
+ "position": {"line": 91, "character": 2}}
 {"range":
- {"start": {"line": 86, "character": 0}, "end": {"line": 86, "character": 7}},
+ {"start": {"line": 91, "character": 0}, "end": {"line": 91, "character": 7}},
  "contents": {"value": "My command ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 89, "character": 16}}
+ "position": {"line": 94, "character": 16}}
 {"range":
- {"start": {"line": 89, "character": 16}, "end": {"line": 89, "character": 23}},
+ {"start": {"line": 94, "character": 16}, "end": {"line": 94, "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": 89, "character": 24}}
+ "position": {"line": 94, "character": 24}}
 {"range":
- {"start": {"line": 89, "character": 24}, "end": {"line": 89, "character": 31}},
+ {"start": {"line": 94, "character": 24}, "end": {"line": 94, "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": 89, "character": 31}}
+ "position": {"line": 94, "character": 31}}
 {"range":
- {"start": {"line": 89, "character": 31}, "end": {"line": 89, "character": 35}},
+ {"start": {"line": 94, "character": 31}, "end": {"line": 94, "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": 98, "character": 2}}
+ "position": {"line": 103, "character": 2}}
 {"range":
- {"start": {"line": 98, "character": 0}, "end": {"line": 98, "character": 8}},
+ {"start": {"line": 103, "character": 0}, "end": {"line": 103, "character": 8}},
  "contents": {"value": "My ultimate command ", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 102, "character": 10}}
+ "position": {"line": 107, "character": 10}}
 null
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 106, "character": 8}}
+ "position": {"line": 111, "character": 8}}
 {"range":
- {"start": {"line": 106, "character": 8},
-  "end": {"line": 106, "character": 10}},
+ {"start": {"line": 111, "character": 8},
+  "end": {"line": 111, "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": 106, "character": 10}}
+ "position": {"line": 111, "character": 10}}
 {"range":
- {"start": {"line": 106, "character": 8},
-  "end": {"line": 106, "character": 21}},
+ {"start": {"line": 111, "character": 8},
+  "end": {"line": 111, "character": 21}},
  "contents": {"value": "```lean\nTrue\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 113, "character": 2}}
+ "position": {"line": 118, "character": 2}}
 {"range":
- {"start": {"line": 113, "character": 2}, "end": {"line": 113, "character": 3}},
+ {"start": {"line": 118, "character": 2}, "end": {"line": 118, "character": 3}},
  "contents": {"value": "```lean\nn : Id Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 120, "character": 9}}
-{"range":
- {"start": {"line": 120, "character": 7},
-  "end": {"line": 120, "character": 17}},
- "contents": {"value": "```lean\nfoo : Nat\n```", "kind": "markdown"}}
-{"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 125, "character": 7}}
+ "position": {"line": 125, "character": 9}}
 {"range":
  {"start": {"line": 125, "character": 7},
-  "end": {"line": 125, "character": 10}},
+  "end": {"line": 125, "character": 17}},
+ "contents": {"value": "```lean\nfoo : Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 130, "character": 7}}
+{"range":
+ {"start": {"line": 130, "character": 7},
+  "end": {"line": 130, "character": 10}},
  "contents": {"value": "```lean\nBar.foo : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 128, "character": 9}}
+ "position": {"line": 133, "character": 9}}
 {"range":
- {"start": {"line": 128, "character": 7},
-  "end": {"line": 128, "character": 17}},
+ {"start": {"line": 133, "character": 7},
+  "end": {"line": 133, "character": 17}},
  "contents": {"value": "```lean\n_root_.foo : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 131, "character": 4}}
+ "position": {"line": 136, "character": 4}}
 {"range":
- {"start": {"line": 131, "character": 4}, "end": {"line": 131, "character": 7}},
+ {"start": {"line": 136, "character": 4}, "end": {"line": 136, "character": 7}},
  "contents": {"value": "```lean\nBar.bar : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 134, "character": 10}}
+ "position": {"line": 139, "character": 10}}
 {"range":
- {"start": {"line": 134, "character": 10},
-  "end": {"line": 134, "character": 13}},
+ {"start": {"line": 139, "character": 10},
+  "end": {"line": 139, "character": 13}},
  "contents": {"value": "```lean\nBar.Foo : Type\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 134, "character": 17}}
+ "position": {"line": 139, "character": 17}}
 {"range":
- {"start": {"line": 134, "character": 17},
-  "end": {"line": 134, "character": 19}},
+ {"start": {"line": 139, "character": 17},
+  "end": {"line": 139, "character": 19}},
  "contents":
  {"value": "```lean\nBar.Foo.mk : Nat → Foo\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 137, "character": 2}}
+ "position": {"line": 142, "character": 2}}
 {"range":
- {"start": {"line": 137, "character": 2}, "end": {"line": 137, "character": 4}},
+ {"start": {"line": 142, "character": 2}, "end": {"line": 142, "character": 4}},
  "contents":
  {"value": "```lean\nBar.Foo.hi : Foo → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 140, "character": 10}}
+ "position": {"line": 145, "character": 10}}
 {"range":
- {"start": {"line": 140, "character": 10},
-  "end": {"line": 140, "character": 13}},
+ {"start": {"line": 145, "character": 10},
+  "end": {"line": 145, "character": 13}},
  "contents": {"value": "```lean\nBar.Bar : Type\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 142, "character": 4}}
+ "position": {"line": 147, "character": 4}}
 {"range":
- {"start": {"line": 142, "character": 4}, "end": {"line": 142, "character": 6}},
+ {"start": {"line": 147, "character": 4}, "end": {"line": 147, "character": 6}},
  "contents": {"value": "```lean\nBar.Bar.mk : Bar\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 145, "character": 2}}
+ "position": {"line": 150, "character": 2}}
 {"range":
- {"start": {"line": 145, "character": 0}, "end": {"line": 145, "character": 8}},
+ {"start": {"line": 150, "character": 0}, "end": {"line": 150, "character": 8}},
  "contents":
  {"value": "```lean\nBar.instToStringNat : ToString Nat\n```",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 147, "character": 9}}
+ "position": {"line": 152, "character": 9}}
 {"range":
- {"start": {"line": 147, "character": 9},
-  "end": {"line": 147, "character": 10}},
+ {"start": {"line": 152, "character": 9},
+  "end": {"line": 152, "character": 10}},
  "contents":
  {"value": "```lean\nBar.f : ToString Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 150, "character": 10}}
+ "position": {"line": 155, "character": 10}}
 {"range":
- {"start": {"line": 150, "character": 10},
-  "end": {"line": 150, "character": 16}},
+ {"start": {"line": 155, "character": 10},
+  "end": {"line": 155, "character": 16}},
  "contents":
  {"value": "A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ",
   "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 153, "character": 4}}
+ "position": {"line": 158, "character": 4}}
 {"range":
- {"start": {"line": 153, "character": 4},
-  "end": {"line": 153, "character": 11}},
+ {"start": {"line": 158, "character": 4},
+  "end": {"line": 158, "character": 11}},
  "contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 153, "character": 8}}
+ "position": {"line": 158, "character": 8}}
 {"range":
- {"start": {"line": 153, "character": 4},
-  "end": {"line": 153, "character": 11}},
+ {"start": {"line": 158, "character": 4},
+  "end": {"line": 158, "character": 11}},
  "contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 158, "character": 6}}
+ "position": {"line": 163, "character": 6}}
 {"range":
- {"start": {"line": 158, "character": 6}, "end": {"line": 158, "character": 7}},
+ {"start": {"line": 163, "character": 6}, "end": {"line": 163, "character": 7}},
  "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 161, "character": 4}}
+ "position": {"line": 166, "character": 4}}
 [{"targetUri": "file://hover.lean",
   "targetSelectionRange":
-  {"start": {"line": 158, "character": 6},
-   "end": {"line": 158, "character": 7}},
+  {"start": {"line": 163, "character": 6},
+   "end": {"line": 163, "character": 7}},
   "targetRange":
-  {"start": {"line": 158, "character": 6},
-   "end": {"line": 158, "character": 7}},
+  {"start": {"line": 163, "character": 6},
+   "end": {"line": 163, "character": 7}},
   "originSelectionRange":
-  {"start": {"line": 161, "character": 4},
-   "end": {"line": 161, "character": 5}}}]
+  {"start": {"line": 166, "character": 4},
+   "end": {"line": 166, "character": 5}}}]
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 161, "character": 4}}
+ "position": {"line": 166, "character": 4}}
 {"range":
- {"start": {"line": 161, "character": 4}, "end": {"line": 161, "character": 5}},
+ {"start": {"line": 166, "character": 4}, "end": {"line": 166, "character": 5}},
  "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 165, "character": 8}}
+ "position": {"line": 170, "character": 8}}
 {"range":
- {"start": {"line": 165, "character": 8}, "end": {"line": 165, "character": 9}},
+ {"start": {"line": 170, "character": 8}, "end": {"line": 170, "character": 9}},
  "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 168, "character": 8}}
+ "position": {"line": 173, "character": 8}}
 [{"targetUri": "file://hover.lean",
   "targetSelectionRange":
-  {"start": {"line": 165, "character": 8},
-   "end": {"line": 165, "character": 9}},
+  {"start": {"line": 170, "character": 8},
+   "end": {"line": 170, "character": 9}},
   "targetRange":
-  {"start": {"line": 165, "character": 8},
-   "end": {"line": 165, "character": 9}},
+  {"start": {"line": 170, "character": 8},
+   "end": {"line": 170, "character": 9}},
   "originSelectionRange":
-  {"start": {"line": 168, "character": 8},
-   "end": {"line": 168, "character": 9}}}]
+  {"start": {"line": 173, "character": 8},
+   "end": {"line": 173, "character": 9}}}]
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 168, "character": 8}}
+ "position": {"line": 173, "character": 8}}
 {"range":
- {"start": {"line": 168, "character": 8}, "end": {"line": 168, "character": 9}},
+ {"start": {"line": 173, "character": 8}, "end": {"line": 173, "character": 9}},
  "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 173, "character": 25}}
+ "position": {"line": 178, "character": 25}}
 {"range":
- {"start": {"line": 173, "character": 25},
-  "end": {"line": 173, "character": 26}},
+ {"start": {"line": 178, "character": 25},
+  "end": {"line": 178, "character": 26}},
  "contents": {"value": "```lean\nn : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 176, "character": 2}}
+ "position": {"line": 181, "character": 2}}
 null
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 182, "character": 2}}
+ "position": {"line": 187, "character": 2}}
 {"range":
- {"start": {"line": 182, "character": 2},
-  "end": {"line": 182, "character": 15}},
+ {"start": {"line": 187, "character": 2},
+  "end": {"line": 187, "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": 185, "character": 28}}
+ "position": {"line": 190, "character": 28}}
 {"range":
- {"start": {"line": 185, "character": 27},
-  "end": {"line": 185, "character": 32}},
+ {"start": {"line": 190, "character": 27},
+  "end": {"line": 190, "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",