chore: add completion test for the group issue
This commit is contained in:
parent
95419cc194
commit
2da8e5afa1
2 changed files with 19 additions and 0 deletions
11
tests/lean/interactive/completion5.lean
Normal file
11
tests/lean/interactive/completion5.lean
Normal file
|
|
@ -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
|
||||
8
tests/lean/interactive/completion5.lean.expected.out
Normal file
8
tests/lean/interactive/completion5.lean.expected.out
Normal file
|
|
@ -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}
|
||||
Loading…
Add table
Reference in a new issue