diff --git a/tests/lean/interactive/completionStructureInstance.lean b/tests/lean/interactive/completionStructureInstance.lean index ff79f641c6..a9a084fbf5 100644 --- a/tests/lean/interactive/completionStructureInstance.lean +++ b/tests/lean/interactive/completionStructureInstance.lean @@ -92,5 +92,7 @@ example (s : S) : S := { s with : S } -- All field completions expected example (s : S) : S := { s with f } -- All field completions matching `f` expected --^ textDocument/completion -example (aLongUniqueIdentifier : Nat) : Std.HashSet Nat := { aLongUniqueIdentifier } -- Identifier completion matching `aLongUniqueIdentifier` - --^ textDocument/completion +def aLongUniqueIdentifier := 0 + +example : Std.HashSet Nat := { aLongUniqueIdentifier } -- Identifier completion matching `aLongUniqueIdentifier` + --^ textDocument/completion diff --git a/tests/lean/interactive/completionStructureInstance.lean.expected.out b/tests/lean/interactive/completionStructureInstance.lean.expected.out index aab84e36c0..230c804b64 100644 --- a/tests/lean/interactive/completionStructureInstance.lean.expected.out +++ b/tests/lean/interactive/completionStructureInstance.lean.expected.out @@ -598,15 +598,15 @@ "cPos": 0}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionStructureInstance.lean"}, - "position": {"line": 94, "character": 82}} + "position": {"line": 96, "character": 52}} {"items": [{"sortText": "0", "label": "aLongUniqueIdentifier", - "kind": 6, + "kind": 21, "data": {"params": {"textDocument": {"uri": "file:///completionStructureInstance.lean"}, - "position": {"line": 94, "character": 82}}, - "id": {"fvar": {"id": "_uniq.1028"}}, + "position": {"line": 96, "character": 52}}, + "id": {"const": {"declName": "aLongUniqueIdentifier"}}, "cPos": 0}}], "isIncomplete": true}