max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: completion

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-12 22:32:27 -07:00
parent 40a42128be
commit d2910337af
2 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/interactive/completion7.lean Normal file
View file

@ -0,0 +1,4 @@
#check And
--^ textDocument/completion
#check And.
--^ textDocument/completion

14
tests/lean/interactive/completion7.lean.expected.out Normal file
View file

@ -0,0 +1,14 @@
{"textDocument": {"uri": "file://completion7.lean"},
"position": {"line": 0, "character": 10}}
{"items":
[{"label": "And", "detail": "Prop → Prop → Prop"},
{"label": "AndOp", "detail": "Type u → Type u"},
{"label": "AndThen", "detail": "Type u → Type u"}],
"isIncomplete": true}
{"textDocument": {"uri": "file://completion7.lean"},
"position": {"line": 2, "character": 11}}
{"items":
[{"label": "intro", "detail": "?a → ?b → ?a ∧ ?b"},
{"label": "left", "detail": "?a ∧ ?b → ?a"},
{"label": "right", "detail": "?a ∧ ?b → ?b"}],
"isIncomplete": true}