From 43e107ef67dd02caeef3e91cccc0ae960d0beb7d Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 8 Feb 2024 17:05:27 +1100
Subject: [PATCH] chore: test for no goal sorry

---
 test/no_goal_sorry.expected.out | 11 +++++++++++
 test/no_goal_sorry.in           |  1 +
 2 files changed, 12 insertions(+)
 create mode 100644 test/no_goal_sorry.expected.out
 create mode 100644 test/no_goal_sorry.in

diff --git a/test/no_goal_sorry.expected.out b/test/no_goal_sorry.expected.out
new file mode 100644
index 0000000..5be11b7
--- /dev/null
+++ 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
new file mode 100644
index 0000000..7f55630
--- /dev/null
+++ b/test/no_goal_sorry.in
@@ -0,0 +1 @@
+{"cmd" : "example : True := by\n  have h : set Nat := by sorry\n  sorry"}