diff --git a/tests/lean/interactive/completion5.lean b/tests/lean/interactive/completion5.lean
new file mode 100644
index 0000000000..5d9fffe661
--- /dev/null
+++ b/tests/lean/interactive/completion5.lean
@@ -0,0 +1,11 @@
+structure C where
+  f1 : Nat
+  f2 : Bool
+  b1 : String
+
+def f (c : C) : IO Unit :=
+  visit c
+where
+  visit (c : C) : IO Unit :=
+    let x := c.
+             --^ textDocument/completion
diff --git a/tests/lean/interactive/completion5.lean.expected.out b/tests/lean/interactive/completion5.lean.expected.out
new file mode 100644
index 0000000000..c3f14336b9
--- /dev/null
+++ b/tests/lean/interactive/completion5.lean.expected.out
@@ -0,0 +1,8 @@
+{"textDocument": {"uri": "file://completion5.lean"},
+ "position": {"line": 9, "character": 15}}
+{"items":
+ [{"label": "mk", "detail": "Nat → Bool → String → C"},
+  {"label": "b1", "detail": "C → String"},
+  {"label": "f1", "detail": "C → Nat"},
+  {"label": "f2", "detail": "C → Bool"}],
+ "isIncomplete": true}