0602b805c8
`with` considered harmful when merging old and new state, let's always be explicit in these cases
36 lines
1.3 KiB
Text
36 lines
1.3 KiB
Text
{"version": 2, "uri": "file:///incrementalCommand.lean", "diagnostics": []}
|
|
{"version": 2, "uri": "file:///incrementalCommand.lean", "diagnostics": []}
|
|
w
|
|
w
|
|
{"version": 1, "uri": "file:///incrementalCommand.lean", "diagnostics": []}
|
|
{"version": 1,
|
|
"uri": "file:///incrementalCommand.lean",
|
|
"diagnostics":
|
|
[{"source": "Lean 4",
|
|
"severity": 3,
|
|
"range":
|
|
{"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}},
|
|
"message": "\"import\"\n",
|
|
"fullRange":
|
|
{"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}}]}
|
|
{"version": 2,
|
|
"uri": "file:///incrementalCommand.lean",
|
|
"diagnostics":
|
|
[{"source": "Lean 4",
|
|
"severity": 3,
|
|
"range":
|
|
{"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}},
|
|
"message": "\"import\"\n",
|
|
"fullRange":
|
|
{"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}}]}
|
|
{"version": 2,
|
|
"uri": "file:///incrementalCommand.lean",
|
|
"diagnostics":
|
|
[{"source": "Lean 4",
|
|
"severity": 1,
|
|
"range":
|
|
{"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 9}},
|
|
"message": "tactic 'assumption' failed\n⊢ False",
|
|
"fullRange":
|
|
{"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 9}}}]}
|
|
{"version": 3, "uri": "file:///incrementalCommand.lean", "diagnostics": []}
|