mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
a3cb39eac9
This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
66 lines
2.2 KiB
Plaintext
66 lines
2.2 KiB
Plaintext
[{"item":
|
|
{"uri": "file:///incomingCallHierarchyWhere.lean",
|
|
"selectionRange":
|
|
{"start": {"line": 8, "character": 4}, "end": {"line": 8, "character": 5}},
|
|
"range":
|
|
{"start": {"line": 8, "character": 4}, "end": {"line": 8, "character": 5}},
|
|
"name": "f",
|
|
"kind": 14,
|
|
"data":
|
|
{"name": "f",
|
|
"module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
|
|
"fromRanges": [],
|
|
"children":
|
|
[{"item":
|
|
{"uri": "file:///incomingCallHierarchyWhere.lean",
|
|
"selectionRange":
|
|
{"start": {"line": 14, "character": 2},
|
|
"end": {"line": 14, "character": 5}},
|
|
"range":
|
|
{"start": {"line": 14, "character": 2},
|
|
"end": {"line": 14, "character": 16}},
|
|
"name": "foo.bar",
|
|
"kind": 14,
|
|
"data":
|
|
{"name":
|
|
"_private.«external:file:///incomingCallHierarchyWhere.lean».0.foo.bar",
|
|
"module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
|
|
"fromRanges":
|
|
[{"start": {"line": 14, "character": 15},
|
|
"end": {"line": 14, "character": 16}}],
|
|
"children":
|
|
[{"item":
|
|
{"uri": "file:///incomingCallHierarchyWhere.lean",
|
|
"selectionRange":
|
|
{"start": {"line": 11, "character": 4},
|
|
"end": {"line": 11, "character": 7}},
|
|
"range":
|
|
{"start": {"line": 11, "character": 0},
|
|
"end": {"line": 14, "character": 16}},
|
|
"name": "foo",
|
|
"kind": 14,
|
|
"data":
|
|
{"name": "foo",
|
|
"module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
|
|
"fromRanges":
|
|
[{"start": {"line": 12, "character": 2},
|
|
"end": {"line": 12, "character": 5}}],
|
|
"children":
|
|
[{"item":
|
|
{"uri": "file:///incomingCallHierarchyWhere.lean",
|
|
"selectionRange":
|
|
{"start": {"line": 16, "character": 4},
|
|
"end": {"line": 16, "character": 10}},
|
|
"range":
|
|
{"start": {"line": 16, "character": 0},
|
|
"end": {"line": 16, "character": 17}},
|
|
"name": "foobar",
|
|
"kind": 14,
|
|
"data":
|
|
{"name": "foobar",
|
|
"module": "«external:file:///incomingCallHierarchyWhere.lean»"}},
|
|
"fromRanges":
|
|
[{"start": {"line": 16, "character": 14},
|
|
"end": {"line": 16, "character": 17}}],
|
|
"children": []}]}]}]}]
|