diff --git a/tests/lean/interactive/533.lean b/tests/lean/interactive/533.lean
index 8f2cbf6083..40bf4a2f2e 100644
--- a/tests/lean/interactive/533.lean
+++ b/tests/lean/interactive/533.lean
@@ -1,3 +1,5 @@
+prelude
+
 set_option relaxedAutoImplicit false
 inductive Foo where
  | bar : F
diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out
index 35b73188bd..f9137c9288 100644
--- a/tests/lean/interactive/533.lean.expected.out
+++ b/tests/lean/interactive/533.lean.expected.out
@@ -1,125 +1,6 @@
 {"textDocument": {"uri": "file://533.lean"},
- "position": {"line": 2, "character": 10}}
+ "position": {"line": 4, "character": 10}}
 {"items":
  [{"label": "F", "kind": 6, "detail": "Sort ?u"},
-  {"label": "False",
-   "kind": 22,
-   "documentation":
-   {"value":
-    "`False` is the empty proposition. Thus, it has no introduction rules.\nIt represents a contradiction. `False` elimination rule, `False.rec`,\nexpresses the fact that anything follows from a contradiction.\nThis rule is sometimes called ex falso (short for ex falso sequitur quodlibet),\nor the principle of explosion.\nFor more information: [Propositional Logic](https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)\n",
-    "kind": "markdown"},
-   "detail": "Prop"},
-  {"label": "Fin",
-   "kind": 22,
-   "documentation":
-   {"value":
-    "`Fin n` is a natural number `i` with the constraint that `0 ≤ i < n`.\nIt is the \"canonical type with `n` elements\".\n",
-    "kind": "markdown"},
-   "detail": "Nat → Type"},
-  {"label": "Float", "kind": 22, "detail": "Type"},
-  {"label": "FloatArray", "kind": 22, "detail": "Type"},
-  {"label": "FloatSpec", "kind": 22, "detail": "Type 1"},
-  {"label": "Foo", "kind": 6, "detail": "Sort ?u"},
-  {"label": "ForIn",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "`ForIn m ρ α` is the typeclass which supports `for x in xs` notation.\nHere `xs : ρ` is the type of the collection to iterate over, `x : α`\nis the element type which is made available inside the loop, and `m` is the monad\nfor the encompassing `do` block.\n",
-    "kind": "markdown"},
-   "detail":
-   "(Type u₁ → Type u₂) → Type u → outParam (Type v) → Type (max (max (max u (u₁ + 1)) u₂) v)"},
-  {"label": "ForIn'",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "`ForIn' m ρ α d` is a variation on the `ForIn m ρ α` typeclass which supports the\n`for h : x in xs` notation. It is the same as `for x in xs` except that `h : x ∈ xs`\nis provided as an additional argument to the body of the for-loop.\n",
-    "kind": "markdown"},
-   "detail":
-   "(Type u₁ → Type u₂) →\n  (ρ : Type u) → (α : outParam (Type v)) → outParam (Membership α ρ) → Type (max (max (max u (u₁ + 1)) u₂) v)"},
-  {"label": "ForInStep",
-   "kind": 22,
-   "documentation":
-   {"value":
-    "Auxiliary type used to compile `for x in xs` notation.\n\nThis is the return value of the body of a `ForIn` call,\nrepresenting the body of a for loop. It can be:\n\n* `.yield (a : α)`, meaning that we should continue the loop and `a` is the new state.\n  `.yield` is produced by `continue` and reaching the bottom of the loop body.\n* `.done (a : α)`, meaning that we should early-exit the loop with state `a`.\n  `.done` is produced by calls to `break` or `return` in the loop,\n",
-    "kind": "markdown"},
-   "detail": "Type u → Type u"},
-  {"label": "ForM",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "Typeclass for the polymorphic `forM` operation described in the \"do unchained\" paper.\nRemark:\n- `γ` is a \"container\" type of elements of type `α`.\n- `α` is treated as an output parameter by the typeclass resolution procedure.\n  That is, it tries to find an instance using only `m` and `γ`.\n",
-    "kind": "markdown"},
-   "detail":
-   "(Type u → Type v) → Type w₁ → outParam (Type w₂) → Type (max (max (max (u + 1) v) w₁) w₂)"},
-  {"label": "Function", "kind": 9, "detail": "namespace"},
-  {"label": "Functor",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "In functional programming, a \"functor\" is a function on types `F : Type u → Type v`\nequipped with an operator called `map` or `<$>` such that if `f : α → β` then\n`map f : F α → F β`, so `f <$> x : F β` if `x : F α`. This corresponds to the\ncategory-theory notion of [functor](https://en.wikipedia.org/wiki/Functor) in\nthe special case where the category is the category of types and functions\nbetween them, except that this class supplies only the operations and not the\nlaws (see `LawfulFunctor`).\n",
-    "kind": "markdown"},
-   "detail": "(Type u → Type v) → Type (max (u + 1) v)"},
-  {"label": "failure",
-   "kind": 5,
-   "detail": "[self : Alternative f] → {α : Type u} → f α"},
-  {"label": "false",
-   "kind": 4,
-   "documentation":
-   {"value":
-    "The boolean value `false`, not to be confused with the proposition `False`. ",
-    "kind": "markdown"},
-   "detail": "Bool"},
-  {"label": "false_and",
-   "kind": 3,
-   "detail": "∀ (p : Prop), (False ∧ p) = False"},
-  {"label": "false_iff", "kind": 3, "detail": "∀ (p : Prop), (False ↔ p) = ¬p"},
-  {"label": "false_implies",
-   "kind": 3,
-   "detail": "∀ (p : Prop), (False → p) = True"},
-  {"label": "false_of_ne", "kind": 3, "detail": "a ≠ a → False"},
-  {"label": "false_or", "kind": 3, "detail": "∀ (p : Prop), (False ∨ p) = p"},
-  {"label": "flip",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "`flip f a b` is `f b a`. It is useful for \"point-free\" programming,\nsince it can sometimes be used to avoid introducing variables.\nFor example, `(·<·)` is the less-than relation,\nand `flip (·<·)` is the greater-than relation.\n",
-    "kind": "markdown"},
-   "detail": "(α → β → φ) → β → α → φ"},
-  {"label": "floatDecLe",
-   "kind": 3,
-   "detail": "(a b : Float) → Decidable (a ≤ b)"},
-  {"label": "floatDecLt",
-   "kind": 3,
-   "detail": "(a b : Float) → Decidable (a < b)"},
-  {"label": "floatSpec", "kind": 21, "detail": "FloatSpec"},
-  {"label": "forIn",
-   "kind": 5,
-   "documentation":
-   {"value":
-    "`forIn x b f : m β` runs a for-loop in the monad `m` with additional state `β`.\nThis traverses over the \"contents\" of `x`, and passes the elements `a : α` to\n`f : α → β → m (ForInStep β)`. `b : β` is the initial state, and the return value\nof `f` is the new state as well as a directive `.done` or `.yield`\nwhich indicates whether to abort early or continue iteration.\n\nThe expression\n```\nlet mut b := ...\nfor x in xs do\n  b ← foo x b\n```\nin a `do` block is syntactic sugar for:\n```\nlet b := ...\nlet b ← forIn xs b (fun x b => do\n  let b ← foo x b\n  return .yield b)\n```\n(Here `b` corresponds to the variables mutated in the loop.) ",
-    "kind": "markdown"},
-   "detail":
-   "[self : ForIn m ρ α] → {β : Type u₁} → [inst : Monad m] → ρ → β → (α → β → m (ForInStep β)) → m β"},
-  {"label": "forIn'",
-   "kind": 5,
-   "documentation":
-   {"value":
-    "`forIn' x b f : m β` runs a for-loop in the monad `m` with additional state `β`.\nThis traverses over the \"contents\" of `x`, and passes the elements `a : α` along\nwith a proof that `a ∈ x` to `f : (a : α) → a ∈ x → β → m (ForInStep β)`.\n`b : β` is the initial state, and the return value\nof `f` is the new state as well as a directive `.done` or `.yield`\nwhich indicates whether to abort early or continue iteration. ",
-    "kind": "markdown"},
-   "detail":
-   "[self : ForIn' m ρ α d] → {β : Type u₁} → [inst : Monad m] → (x : ρ) → β → ((a : α) → a ∈ x → β → m (ForInStep β)) → m β"},
-  {"label": "forM",
-   "kind": 5,
-   "detail":
-   "[self : ForM m γ α] → [inst : Monad m] → γ → (α → m PUnit) → m PUnit"},
-  {"label": "forall_congr",
-   "kind": 3,
-   "detail": "(∀ (a : α), p a = q a) → (∀ (a : α), p a) = ∀ (a : α), q a"},
-  {"label": "funext",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "**Function extensionality** is the statement that if two functions take equal values\nevery point, then the functions themselves are equal: `(∀ x, f x = g x) → f = g`.\nIt is called \"extensionality\" because it talks about how to prove two objects are equal\nbased on the properties of the object (compare with set extensionality,\nwhich is `(∀ x, x ∈ s ↔ x ∈ t) → s = t`).\n\nThis is often an axiom in dependent type theory systems, because it cannot be proved\nfrom the core logic alone. However in lean's type theory this follows from the existence\nof quotient types (note the `Quot.sound` in the proof, as well as the `show` line\nwhich makes use of the definitional equality `Quot.lift f h (Quot.mk x) = f x`).\n",
-    "kind": "markdown"},
-   "detail": "(∀ (x : α), f x = g x) → f = g"}],
+  {"label": "Foo", "kind": 6, "detail": "Sort ?u"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/863.lean b/tests/lean/interactive/863.lean
index 88a41eeb71..c0a113a488 100644
--- a/tests/lean/interactive/863.lean
+++ b/tests/lean/interactive/863.lean
@@ -1,4 +1,10 @@
-import Lean
+prelude
+
+namespace Lean
+class MonadRef where
+  getRef : Type
+export MonadRef (getRef)
+end Lean
 
 open Lean in
 #check getRe
diff --git a/tests/lean/interactive/863.lean.expected.out b/tests/lean/interactive/863.lean.expected.out
index c274cf900a..bc2651a518 100644
--- a/tests/lean/interactive/863.lean.expected.out
+++ b/tests/lean/interactive/863.lean.expected.out
@@ -1,94 +1,10 @@
 {"textDocument": {"uri": "file://863.lean"},
- "position": {"line": 3, "character": 12}}
+ "position": {"line": 9, "character": 12}}
 {"items":
- [{"label": "getReducibilityStatus",
-   "kind": 3,
-   "documentation":
-   {"value": "Return the reducibility attribute for the given declaration. ",
-    "kind": "markdown"},
-   "detail":
-   "[inst : Monad m] → [inst : MonadEnv m] → Name → m ReducibilityStatus"},
-  {"label": "getRef",
-   "kind": 5,
-   "documentation":
-   {"value": "Get the current value of the `ref` ", "kind": "markdown"},
-   "detail": "[self : MonadRef m] → m Syntax"},
-  {"label": "getRefPos",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "Return the position (as `String.pos`) associated with the current reference syntax (i.e., the syntax object returned by `getRef`.)\n",
-    "kind": "markdown"},
-   "detail": "[inst : Monad m] → [inst : MonadLog m] → m String.Pos"},
-  {"label": "getRefPosition",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "Return the line and column numbers associated with the current reference syntax (i.e., the syntax object returned by `getRef`.)\n",
-    "kind": "markdown"},
-   "detail": "[inst : Monad m] → [inst : MonadLog m] → m Position"},
-  {"label": "getRevAliases",
-   "kind": 3,
-   "detail": "Environment → Name → List Name"},
-  {"label": "getRecAppSyntax?",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "Retrieve (if available) the syntax object attached to a recursive application.\n",
-    "kind": "markdown"},
-   "detail": "Expr → Option Syntax"},
-  {"label": "getRegularInitFnNameFor?",
-   "kind": 3,
-   "detail": "Environment → Name → Option Name"},
-  {"label": "getConstInfoRec",
-   "kind": 3,
-   "detail":
-   "[inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m RecursorVal"}],
+ [{"label": "getRef", "kind": 5, "detail": "[self : MonadRef] → Type"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://863.lean"},
- "position": {"line": 7, "character": 12}}
+ "position": {"line": 13, "character": 12}}
 {"items":
- [{"label": "getReducibilityStatus",
-   "kind": 3,
-   "documentation":
-   {"value": "Return the reducibility attribute for the given declaration. ",
-    "kind": "markdown"},
-   "detail":
-   "[inst : Monad m] → [inst : MonadEnv m] → Name → m ReducibilityStatus"},
-  {"label": "getRef",
-   "kind": 5,
-   "documentation":
-   {"value": "Get the current value of the `ref` ", "kind": "markdown"},
-   "detail": "[self : MonadRef m] → m Syntax"},
-  {"label": "getRefPos",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "Return the position (as `String.pos`) associated with the current reference syntax (i.e., the syntax object returned by `getRef`.)\n",
-    "kind": "markdown"},
-   "detail": "[inst : Monad m] → [inst : MonadLog m] → m String.Pos"},
-  {"label": "getRefPosition",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "Return the line and column numbers associated with the current reference syntax (i.e., the syntax object returned by `getRef`.)\n",
-    "kind": "markdown"},
-   "detail": "[inst : Monad m] → [inst : MonadLog m] → m Position"},
-  {"label": "getRevAliases",
-   "kind": 3,
-   "detail": "Environment → Name → List Name"},
-  {"label": "getRecAppSyntax?",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "Retrieve (if available) the syntax object attached to a recursive application.\n",
-    "kind": "markdown"},
-   "detail": "Expr → Option Syntax"},
-  {"label": "getRegularInitFnNameFor?",
-   "kind": 3,
-   "detail": "Environment → Name → Option Name"},
-  {"label": "getConstInfoRec",
-   "kind": 3,
-   "detail":
-   "[inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m RecursorVal"}],
+ [{"label": "getRef", "kind": 5, "detail": "[self : MonadRef] → Type"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/completion7.lean b/tests/lean/interactive/completion7.lean
index 2c2abc6a51..2ff061d568 100644
--- a/tests/lean/interactive/completion7.lean
+++ b/tests/lean/interactive/completion7.lean
@@ -1,3 +1,9 @@
+prelude
+
+structure And where
+  left : Type
+  right : Type
+
 #check And
         --^ textDocument/completion
 #check And.
diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out
index 2e2d053325..f50c1efce9 100644
--- a/tests/lean/interactive/completion7.lean.expected.out
+++ b/tests/lean/interactive/completion7.lean.expected.out
@@ -1,128 +1,11 @@
 {"textDocument": {"uri": "file://completion7.lean"},
- "position": {"line": 0, "character": 10}}
-{"items":
- [{"label": "And",
-   "kind": 22,
-   "documentation":
-   {"value":
-    "`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be\nconstructed and destructed like a pair: if `ha : a` and `hb : b` then\n`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.\n",
-    "kind": "markdown"},
-   "detail": "Prop → Prop → Prop"},
-  {"label": "and",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "`and x y`, or `x && y`, is the boolean \"and\" operation (not to be confused\nwith `And : Prop → Prop → Prop`, which is the propositional connective).\nIt is `@[macro_inline]` because it has C-like short-circuiting behavior:\nif `x` is false then `y` is not evaluated.\n",
-    "kind": "markdown"},
-   "detail": "Bool → Bool → Bool"},
-  {"label": "AndOp",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "The homogeneous version of `HAnd`: `a &&& b : α` where `a b : α`.\n(It is called `AndOp` because `And` is taken for the propositional connective.)\n",
-    "kind": "markdown"},
-   "detail": "Type u → Type u"},
-  {"label": "AndThen",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "The homogeneous version of `HAndThen`: `a >> b : α` where `a b : α`.\nBecause `b` is \"lazy\" in this notation, it is passed as `Unit → α` to the\nimplementation so it can decide when to evaluate it.\n",
-    "kind": "markdown"},
-   "detail": "Type u → Type u"},
-  {"label": "andM",
-   "kind": 3,
-   "detail": "[inst : Monad m] → [inst : ToBool β] → m β → m β → m β"},
-  {"label": "false_and",
-   "kind": 3,
-   "detail": "∀ (p : Prop), (False ∧ p) = False"},
-  {"label": "true_and", "kind": 3, "detail": "∀ (p : Prop), (True ∧ p) = p"},
-  {"label": "HAnd",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "The typeclass behind the notation `a &&& b : γ` where `a : α`, `b : β`. ",
-    "kind": "markdown"},
-   "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"},
-  {"label": "and_false",
-   "kind": 3,
-   "detail": "∀ (p : Prop), (p ∧ False) = False"},
-  {"label": "and_self", "kind": 3, "detail": "∀ (p : Prop), (p ∧ p) = p"},
-  {"label": "and_true", "kind": 3, "detail": "∀ (p : Prop), (p ∧ True) = p"},
-  {"label": "strictAnd",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "`strictAnd` is the same as `and`, but it does not use short-circuit evaluation semantics:\nboth sides are evaluated, even if the first value is `false`.\n",
-    "kind": "markdown"},
-   "detail": "Bool → Bool → Bool"},
-  {"label": "instDecidableAnd",
-   "kind": 3,
-   "detail": "[dp : Decidable p] → [dq : Decidable q] → Decidable (p ∧ q)"},
-  {"label": "instHAnd", "kind": 3, "detail": "[inst : AndOp α] → HAnd α α α"},
-  {"label": "Append",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "The homogeneous version of `HAppend`: `a ++ b : α` where `a b : α`. ",
-    "kind": "markdown"},
-   "detail": "Type u → Type u"},
-  {"label": "HAndThen",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "The typeclass behind the notation `a >> b : γ` where `a : α`, `b : β`.\nBecause `b` is \"lazy\" in this notation, it is passed as `Unit → β` to the\nimplementation so it can decide when to evaluate it.\n",
-    "kind": "markdown"},
-   "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"},
-  {"label": "instAndOpUInt16", "kind": 21, "detail": "AndOp UInt16"},
-  {"label": "instAndOpUInt32", "kind": 21, "detail": "AndOp UInt32"},
-  {"label": "instAndOpUInt64", "kind": 21, "detail": "AndOp UInt64"},
-  {"label": "instAndOpUInt8", "kind": 21, "detail": "AndOp UInt8"},
-  {"label": "instAndOpUSize", "kind": 21, "detail": "AndOp USize"},
-  {"label": "instHAndThen",
-   "kind": 3,
-   "detail": "[inst : AndThen α] → HAndThen α α α"},
-  {"label": "compareOfLessAndEq",
-   "kind": 3,
-   "detail":
-   "(x y : α) → [inst : LT α] → [inst : Decidable (x < y)] → [inst : DecidableEq α] → Ordering"},
-  {"label": "iff_iff_implies_and_implies",
-   "kind": 3,
-   "detail": "∀ (a b : Prop), (a ↔ b) ↔ (a → b) ∧ (b → a)"},
-  {"label": "HAppend",
-   "kind": 7,
-   "documentation":
-   {"value":
-    "The notation typeclass for heterogeneous append.\nThis enables the notation `a ++ b : γ` where `a : α`, `b : β`.\n",
-    "kind": "markdown"},
-   "detail": "Type u → Type v → outParam (Type w) → Type (max (max u v) w)"},
-  {"label": "instAppendSubarray", "kind": 3, "detail": "Append (Subarray α)"},
-  {"label": "instHAppend",
-   "kind": 3,
-   "detail": "[inst : Append α] → HAppend α α α"}],
+ "position": {"line": 6, "character": 10}}
+{"items": [{"label": "And", "kind": 22, "detail": "Type 1"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://completion7.lean"},
- "position": {"line": 2, "character": 11}}
+ "position": {"line": 8, "character": 11}}
 {"items":
- [{"label": "comm", "kind": 3, "detail": "a ∧ b ↔ b ∧ a"},
-  {"label": "intro",
-   "kind": 4,
-   "documentation":
-   {"value":
-    "`And.intro : a → b → a ∧ b` is the constructor for the And operation. ",
-    "kind": "markdown"},
-   "detail": "a → b → a ∧ b"},
-  {"label": "left",
-   "kind": 5,
-   "documentation":
-   {"value":
-    "Extract the left conjunct from a conjunction. `h : a ∧ b` then\n`h.left`, also notated as `h.1`, is a proof of `a`. ",
-    "kind": "markdown"},
-   "detail": "a ∧ b → a"},
-  {"label": "right",
-   "kind": 5,
-   "documentation":
-   {"value":
-    "Extract the right conjunct from a conjunction. `h : a ∧ b` then\n`h.right`, also notated as `h.2`, is a proof of `b`. ",
-    "kind": "markdown"},
-   "detail": "a ∧ b → b"}],
+ [{"label": "left", "kind": 5, "detail": "And → Type"},
+  {"label": "mk", "kind": 4, "detail": "Type → Type → And"},
+  {"label": "right", "kind": 5, "detail": "And → Type"}],
  "isIncomplete": true}
diff --git a/tests/lean/interactive/keywordCompletion.lean b/tests/lean/interactive/keywordCompletion.lean
index 6ecd8449aa..1ac865d268 100644
--- a/tests/lean/interactive/keywordCompletion.lean
+++ b/tests/lean/interactive/keywordCompletion.lean
@@ -1,9 +1,7 @@
-def regular := 0
+prelude
 
-macro "register_string " s:str : term => s
+def bin := Type
 
-#check register_
-              --^ textDocument/completion
-
-#check register_
+#check binop_
         --^ textDocument/completion
+           --^ textDocument/completion
diff --git a/tests/lean/interactive/keywordCompletion.lean.expected.out b/tests/lean/interactive/keywordCompletion.lean.expected.out
index 5b378eb440..001ac9cc14 100644
--- a/tests/lean/interactive/keywordCompletion.lean.expected.out
+++ b/tests/lean/interactive/keywordCompletion.lean.expected.out
@@ -1,21 +1,13 @@
 {"textDocument": {"uri": "file://keywordCompletion.lean"},
- "position": {"line": 4, "character": 16}}
+ "position": {"line": 4, "character": 10}}
 {"items":
- [{"label": "register_string", "kind": 14, "detail": "keyword"},
-  {"label": "termRegister_string_", "kind": 21, "detail": "Lean.ParserDescr"}],
+ [{"label": "bin", "kind": 21, "detail": "Type 1"},
+  {"label": "binop%", "kind": 14, "detail": "keyword"},
+  {"label": "binop_lazy%", "kind": 14, "detail": "keyword"},
+  {"label": "binrel%", "kind": 14, "detail": "keyword"},
+  {"label": "binrel_no_prop%", "kind": 14, "detail": "keyword"}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file://keywordCompletion.lean"},
- "position": {"line": 7, "character": 10}}
-{"items":
- [{"label": "register_string", "kind": 14, "detail": "keyword"},
-  {"label": "regular", "kind": 21, "detail": "Nat"},
-  {"label": "reprArg", "kind": 3, "detail": "[inst : Repr α] → α → Std.Format"},
-  {"label": "termRegister_string_", "kind": 21, "detail": "Lean.ParserDescr"},
-  {"label": "recSubsingleton",
-   "kind": 3,
-   "detail":
-   "∀ [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)]\n  [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)], Subsingleton (Decidable.casesOn h h₂ h₁)"},
-  {"label": "instReprString", "kind": 21, "detail": "Repr String"},
-  {"label": "instReprSubstring", "kind": 21, "detail": "Repr Substring"},
-  {"label": "instReprAtomString", "kind": 21, "detail": "ReprAtom String"}],
+ "position": {"line": 4, "character": 13}}
+{"items": [{"label": "binop_lazy%", "kind": 14, "detail": "keyword"}],
  "isIncomplete": true}