{"version": 1,
 "uri": "file:///interactiveDiagnostics.lean",
 "isIncremental": false,
 "diagnostics":
 [{"source": "Lean 4",
   "severity": 2,
   "range":
   {"start": {"line": 0, "character": 4}, "end": {"line": 0, "character": 7}},
   "message": "declaration uses `sorry`",
   "fullRange":
   {"start": {"line": 0, "character": 4}, "end": {"line": 0, "character": 7}}},
  {"source": "Lean 4",
   "severity": 1,
   "range":
   {"start": {"line": 2, "character": 4}, "end": {"line": 2, "character": 7}},
   "message": "Failed to infer type of definition `bar`",
   "fullRange":
   {"start": {"line": 2, "character": 4}, "end": {"line": 2, "character": 7}},
   "code": "lean.inferDefTypeFailed"},
  {"source": "Lean 4",
   "severity": 3,
   "range":
   {"start": {"line": 4, "character": 0}, "end": {"line": 4, "character": 5}},
   "message": "1",
   "fullRange":
   {"start": {"line": 4, "character": 0}, "end": {"line": 4, "character": 5}}},
  {"source": "Lean 4",
   "severity": 3,
   "range":
   {"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 6}},
   "message": "Nat : Type",
   "fullRange":
   {"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 6}}}]}
{"lineRange": {"start": 0, "end": 8}}
[{"source": "Lean 4",
  "severity": 2,
  "range":
  {"start": {"line": 0, "character": 4}, "end": {"line": 0, "character": 7}},
  "message":
  {"append":
   [{"tag": [{"expr": {"text": "declaration uses `"}}, {"text": ""}]},
    {"tag":
     [{"expr":
       {"tag":
        [{"subexprPos": "/", "info": {"__rpcref": "0"}}, {"text": "sorry"}]}},
      {"text": ""}]},
    {"tag": [{"expr": {"text": "`"}}, {"text": ""}]}]},
  "fullRange":
  {"start": {"line": 0, "character": 4}, "end": {"line": 0, "character": 7}}},
 {"source": "Lean 4",
  "severity": 1,
  "range":
  {"start": {"line": 2, "character": 4}, "end": {"line": 2, "character": 7}},
  "message":
  {"append":
   [{"tag": [{"expr": {"text": "Failed to infer type of "}}, {"text": ""}]},
    {"tag": [{"expr": {"text": "definition `"}}, {"text": ""}]},
    {"tag": [{"expr": {"text": "bar"}}, {"text": ""}]},
    {"tag": [{"expr": {"text": "`"}}, {"text": ""}]},
    {"tag":
     [{"widget":
       {"wi":
        {"props":
         {"explanationUrl":
          "REFERENCE/find/?domain=Manual.errorExplanation&name=lean.inferDefTypeFailed",
          "code": "lean.inferDefTypeFailed"},
         "javascriptHash": "14043757810349425459",
         "id": "Lean.errorDescriptionWidget"},
        "alt": {"tag": [{"expr": {"text": ""}}, {"text": ""}]}}},
      {"text": ""}]}]},
  "fullRange":
  {"start": {"line": 2, "character": 4}, "end": {"line": 2, "character": 7}},
  "code": "lean.inferDefTypeFailed"},
 {"source": "Lean 4",
  "severity": 3,
  "range":
  {"start": {"line": 4, "character": 0}, "end": {"line": 4, "character": 5}},
  "message": {"tag": [{"expr": {"text": "1"}}, {"text": ""}]},
  "fullRange":
  {"start": {"line": 4, "character": 0}, "end": {"line": 4, "character": 5}}},
 {"source": "Lean 4",
  "severity": 3,
  "range":
  {"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 6}},
  "message":
  {"tag":
   [{"expr":
     {"append":
      [{"text": "Nat : "},
       {"tag":
        [{"subexprPos": "/1", "info": {"__rpcref": "0"}}, {"text": "Type"}]}]}},
    {"text": ""}]},
  "fullRange":
  {"start": {"line": 6, "character": 0}, "end": {"line": 6, "character": 6}}}]