b 0
b 1
b 2
b 2.5
t 0
t 1
t 2
t 2
{"version": 3,
 "uri": "file:///incrementalTactic.lean",
 "isIncremental": false,
 "diagnostics":
 [{"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 2, "character": 22}, "end": {"line": 3, "character": 0}},
   "message": "unsolved goals\nthis : ∀ (a a : Nat), True\n⊢ True",
   "leanTags": [1],
   "fullRange":
   {"start": {"line": 2, "character": 22},
    "end": {"line": 10, "character": 11}}},
  {"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 4, "character": 12}, "end": {"line": 4, "character": 13}},
   "message":
   "Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce\n\na n : Nat\n⊢ True",
   "fullRange":
   {"start": {"line": 4, "character": 12},
    "end": {"line": 4, "character": 13}}}]}
{"version": 1,
 "uri": "file:///incrementalTactic.lean",
 "isIncremental": false,
 "diagnostics":
 [{"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 1, "character": 38}, "end": {"line": 4, "character": 3}},
   "message": "unexpected token '/-!'; expected ')', '_', identifier or term",
   "fullRange":
   {"start": {"line": 1, "character": 38},
    "end": {"line": 4, "character": 3}}}]}
{"version": 1,
 "uri": "file:///incrementalTactic.lean",
 "isIncremental": false,
 "diagnostics":
 [{"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 2, "character": 9}, "end": {"line": 2, "character": 11}},
   "message": "Unknown identifier `no`",
   "fullRange":
   {"start": {"line": 2, "character": 9}, "end": {"line": 2, "character": 11}},
   "code": "lean.unknownIdentifier"},
  {"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 3, "character": 9}, "end": {"line": 3, "character": 16}},
   "message": "unsolved goals\n⊢ Nat",
   "leanTags": [1],
   "fullRange":
   {"start": {"line": 3, "character": 9},
    "end": {"line": 3, "character": 16}}}]}
s
{"textDocument": {"uri": "file:///incrementalTactic.lean"},
 "position": {"line": 5, "character": 2}}
{"goals":
 [{"type":
   {"tag": [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "True"}]},
   "mvarId": "[anonymous]",
   "hyps": [],
   "goalPrefix": "⊢ ",
   "ctx": {"__rpcref": "1"}}]}
{"version": 1,
 "uri": "file:///incrementalTactic.lean",
 "isIncremental": false,
 "diagnostics":
 [{"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 2, "character": 8}, "end": {"line": 2, "character": 25}},
   "message":
   "Tactic `rewrite` failed: Did not find an occurrence of the pattern\n  0\nin the target expression\n  True\n\n⊢ True",
   "fullRange":
   {"start": {"line": 2, "character": 8},
    "end": {"line": 2, "character": 25}}}]}
{"version": 1,
 "uri": "file:///incrementalTactic.lean",
 "isIncremental": false,
 "diagnostics":
 [{"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 3, "character": 12}, "end": {"line": 3, "character": 16}},
   "message": "unsolved goals\ncase zero\n⊢ True",
   "leanTags": [1],
   "fullRange":
   {"start": {"line": 3, "character": 12},
    "end": {"line": 3, "character": 16}}}]}
{"version": 2,
 "uri": "file:///incrementalTactic.lean",
 "isIncremental": false,
 "diagnostics":
 [{"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 2, "character": 6}, "end": {"line": 2, "character": 10}},
   "message": "unsolved goals\n⊢ True",
   "leanTags": [1],
   "fullRange":
   {"start": {"line": 2, "character": 6}, "end": {"line": 2, "character": 10}}},
  {"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 3, "character": 4}, "end": {"line": 3, "character": 10}},
   "message": "No goals to be solved",
   "fullRange":
   {"start": {"line": 3, "character": 4}, "end": {"line": 3, "character": 10}}},
  {"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 8}},
   "message": "No goals to be solved",
   "fullRange":
   {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 8}}}]}
{"version": 2,
 "uri": "file:///incrementalTactic.lean",
 "isIncremental": false,
 "diagnostics":
 [{"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 3, "character": 8}, "end": {"line": 3, "character": 21}},
   "message": "Unknown identifier `noSuchTheorem`",
   "fullRange":
   {"start": {"line": 3, "character": 8}, "end": {"line": 3, "character": 21}},
   "code": "lean.unknownIdentifier"}]}