test: fix brittle structure instance completion test (#6127)

#5835 contains a brittle test that uses an FVar ID, which caused a
failure on master. This PR changes that test to use a declaration
instead.
This commit is contained in:
Marc Huisinga 2024-11-19 11:13:51 +01:00 committed by GitHub
parent 4bef3588b5
commit a38566693b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 8 additions and 6 deletions

View file

@ -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

View file

@ -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}