75 lines
2.4 KiB
Text
75 lines
2.4 KiB
Text
{"textDocument": {"version": 2, "uri": "file://editAfterError.lean"},
|
|
"contentChanges":
|
|
[{"text": "s",
|
|
"range":
|
|
{"start": {"line": 1, "character": 10},
|
|
"end": {"line": 1, "character": 11}}}]}
|
|
{"version": 2,
|
|
"uri": "file://editAfterError.lean",
|
|
"diagnostics":
|
|
[{"tags": null,
|
|
"source": "Lean 4",
|
|
"severity": 1,
|
|
"relatedInformation": null,
|
|
"range":
|
|
{"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
|
|
"message": "unknown identifier 'tru'",
|
|
"fullRange":
|
|
{"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
|
|
"code": null},
|
|
{"tags": null,
|
|
"source": "Lean 4",
|
|
"severity": 1,
|
|
"relatedInformation": null,
|
|
"range":
|
|
{"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
|
|
"message": "unknown identifier 'fals'",
|
|
"fullRange":
|
|
{"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
|
|
"code": null}]}
|
|
{"version": 2,
|
|
"uri": "file://editAfterError.lean",
|
|
"diagnostics":
|
|
[{"tags": null,
|
|
"source": "Lean 4",
|
|
"severity": 1,
|
|
"relatedInformation": null,
|
|
"range":
|
|
{"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
|
|
"message": "unknown identifier 'tru'",
|
|
"fullRange":
|
|
{"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
|
|
"code": null},
|
|
{"tags": null,
|
|
"source": "Lean 4",
|
|
"severity": 1,
|
|
"relatedInformation": null,
|
|
"range":
|
|
{"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
|
|
"message": "unknown identifier 'fals'",
|
|
"fullRange":
|
|
{"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
|
|
"code": null}]}
|
|
{"version": 2,
|
|
"uri": "file://editAfterError.lean",
|
|
"diagnostics":
|
|
[{"tags": null,
|
|
"source": "Lean 4",
|
|
"severity": 1,
|
|
"relatedInformation": null,
|
|
"range":
|
|
{"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
|
|
"message": "unknown identifier 'tru'",
|
|
"fullRange":
|
|
{"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
|
|
"code": null},
|
|
{"tags": null,
|
|
"source": "Lean 4",
|
|
"severity": 1,
|
|
"relatedInformation": null,
|
|
"range":
|
|
{"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
|
|
"message": "unknown identifier 'fals'",
|
|
"fullRange":
|
|
{"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
|
|
"code": null}]}
|