Skip to content

Commit da091fc

Browse files
committed
remove unnecessary stuff in test
1 parent 50ff6d9 commit da091fc

File tree

2 files changed

+16
-21
lines changed

2 files changed

+16
-21
lines changed

tests/lean/interactive/completion3.lean

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,3 @@
1-
import Lean
2-
3-
elab "#show " c:command : command => do
4-
IO.println c
5-
61
structure S where
72
x : Nat
83
y : String
Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,112 +1,112 @@
11
{"textDocument": {"uri": "file:///completion3.lean"},
2-
"position": {"line": 12, "character": 9}}
2+
"position": {"line": 7, "character": 9}}
33
{"items":
44
[{"label": "x",
55
"kind": 5,
66
"data":
77
{"params":
88
{"textDocument": {"uri": "file:///completion3.lean"},
9-
"position": {"line": 12, "character": 9}},
9+
"position": {"line": 7, "character": 9}},
1010
"id": {"const": {"declName": "S.x"}},
1111
"cPos": 1}},
1212
{"label": "y",
1313
"kind": 5,
1414
"data":
1515
{"params":
1616
{"textDocument": {"uri": "file:///completion3.lean"},
17-
"position": {"line": 12, "character": 9}},
17+
"position": {"line": 7, "character": 9}},
1818
"id": {"const": {"declName": "S.y"}},
1919
"cPos": 1}},
2020
{"label": "b",
2121
"kind": 5,
2222
"data":
2323
{"params":
2424
{"textDocument": {"uri": "file:///completion3.lean"},
25-
"position": {"line": 12, "character": 9}},
25+
"position": {"line": 7, "character": 9}},
2626
"id": {"const": {"declName": "S.b"}},
2727
"cPos": 1}}],
2828
"isIncomplete": false}
2929
{"textDocument": {"uri": "file:///completion3.lean"},
30-
"position": {"line": 17, "character": 5}}
30+
"position": {"line": 12, "character": 5}}
3131
{"items":
3232
[{"label": "x",
3333
"kind": 5,
3434
"data":
3535
{"params":
3636
{"textDocument": {"uri": "file:///completion3.lean"},
37-
"position": {"line": 17, "character": 5}},
37+
"position": {"line": 12, "character": 5}},
3838
"id": {"const": {"declName": "S.x"}},
3939
"cPos": 1}},
4040
{"label": "y",
4141
"kind": 5,
4242
"data":
4343
{"params":
4444
{"textDocument": {"uri": "file:///completion3.lean"},
45-
"position": {"line": 17, "character": 5}},
45+
"position": {"line": 12, "character": 5}},
4646
"id": {"const": {"declName": "S.y"}},
4747
"cPos": 1}},
4848
{"label": "b",
4949
"kind": 5,
5050
"data":
5151
{"params":
5252
{"textDocument": {"uri": "file:///completion3.lean"},
53-
"position": {"line": 17, "character": 5}},
53+
"position": {"line": 12, "character": 5}},
5454
"id": {"const": {"declName": "S.b"}},
5555
"cPos": 1}}],
5656
"isIncomplete": false}
5757
{"textDocument": {"uri": "file:///completion3.lean"},
58-
"position": {"line": 21, "character": 5}}
58+
"position": {"line": 16, "character": 5}}
5959
{"items":
6060
[{"label": "x",
6161
"kind": 5,
6262
"data":
6363
{"params":
6464
{"textDocument": {"uri": "file:///completion3.lean"},
65-
"position": {"line": 21, "character": 5}},
65+
"position": {"line": 16, "character": 5}},
6666
"id": {"const": {"declName": "S.x"}},
6767
"cPos": 1}},
6868
{"label": "y",
6969
"kind": 5,
7070
"data":
7171
{"params":
7272
{"textDocument": {"uri": "file:///completion3.lean"},
73-
"position": {"line": 21, "character": 5}},
73+
"position": {"line": 16, "character": 5}},
7474
"id": {"const": {"declName": "S.y"}},
7575
"cPos": 1}},
7676
{"label": "b",
7777
"kind": 5,
7878
"data":
7979
{"params":
8080
{"textDocument": {"uri": "file:///completion3.lean"},
81-
"position": {"line": 21, "character": 5}},
81+
"position": {"line": 16, "character": 5}},
8282
"id": {"const": {"declName": "S.b"}},
8383
"cPos": 1}}],
8484
"isIncomplete": false}
8585
{"textDocument": {"uri": "file:///completion3.lean"},
86-
"position": {"line": 25, "character": 5}}
86+
"position": {"line": 20, "character": 5}}
8787
{"items":
8888
[{"label": "x",
8989
"kind": 5,
9090
"data":
9191
{"params":
9292
{"textDocument": {"uri": "file:///completion3.lean"},
93-
"position": {"line": 25, "character": 5}},
93+
"position": {"line": 20, "character": 5}},
9494
"id": {"const": {"declName": "S.x"}},
9595
"cPos": 1}},
9696
{"label": "y",
9797
"kind": 5,
9898
"data":
9999
{"params":
100100
{"textDocument": {"uri": "file:///completion3.lean"},
101-
"position": {"line": 25, "character": 5}},
101+
"position": {"line": 20, "character": 5}},
102102
"id": {"const": {"declName": "S.y"}},
103103
"cPos": 1}},
104104
{"label": "b",
105105
"kind": 5,
106106
"data":
107107
{"params":
108108
{"textDocument": {"uri": "file:///completion3.lean"},
109-
"position": {"line": 25, "character": 5}},
109+
"position": {"line": 20, "character": 5}},
110110
"id": {"const": {"declName": "S.b"}},
111111
"cPos": 1}}],
112112
"isIncomplete": false}

0 commit comments

Comments
 (0)