update test

hhu-adam · Jun 17, 2024 · 693dae1 · 693dae1
1 parent 9bb1d4d
commit 693dae1
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 4 deletions.
diff --git a/tests/lean/4448.lean.expected.out b/tests/lean/4448.lean.expected.out
diff --git a/tests/lean/4448.lean → tests/lean/interactive/4448.lean b/tests/lean/4448.lean → tests/lean/interactive/4448.lean
@@ -1,5 +1,3 @@
-import Lean
-
 @[deprecated]
 theorem hi : True := .intro
 
@@ -9,3 +7,4 @@ theorem hi_self : hi = hi := rfl
 
 example : True := by
   simp [← hi_self, hi]
+                   --^ collectDiagnostics
diff --git a/tests/lean/interactive/4448.lean.expected.out b/tests/lean/interactive/4448.lean.expected.out
@@ -0,0 +1,21 @@
+{"version": 1,
+ "uri": "file:///4448.lean",
+ "diagnostics":
+ [{"tags": [2],
+   "source": "Lean 4",
+   "severity": 2,
+   "range":
+   {"start": {"line": 8, "character": 10}, "end": {"line": 8, "character": 17}},
+   "message": "`hi_self` has been deprecated",
+   "fullRange":
+   {"start": {"line": 8, "character": 10},
+    "end": {"line": 8, "character": 17}}},
+  {"tags": [2],
+   "source": "Lean 4",
+   "severity": 2,
+   "range":
+   {"start": {"line": 8, "character": 19}, "end": {"line": 8, "character": 21}},
+   "message": "`hi` has been deprecated",
+   "fullRange":
+   {"start": {"line": 8, "character": 19},
+    "end": {"line": 8, "character": 21}}}]}