chore: test for no goal sorry

leanprover-community · Feb 8, 2024 · 43e107e · 43e107e
1 parent 57535aa
commit 43e107e
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/test/no_goal_sorry.expected.out b/test/no_goal_sorry.expected.out
@@ -0,0 +1,11 @@
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 2, "column": 11},
+   "endPos": {"line": 2, "column": 18},
+   "data": "type expected, got\n  (set Nat : ?m.8 PUnit)"},
+  {"severity": "error",
+   "pos": {"line": 3, "column": 2},
+   "endPos": {"line": 3, "column": 7},
+   "data": "no goals to be solved"}],
+ "env": 0}
+
diff --git a/test/no_goal_sorry.in b/test/no_goal_sorry.in
@@ -0,0 +1 @@
+{"cmd" : "example : True := by\n  have h : set Nat := by sorry\n  sorry"}
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		{"cmd" : "example : True := by\n have h : set Nat := by sorry\n sorry"}