From 6d83eefde9c7a860f4c0a93824be50a7e919027d Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 17 Jan 2024 14:12:25 +1100
Subject: [PATCH] test of all_goals sorry

---
 test/by_cases.expected.out | 6 ++++++
 test/by_cases.in           | 2 ++
 2 files changed, 8 insertions(+)

diff --git a/test/by_cases.expected.out b/test/by_cases.expected.out
index 684f12f..0530ff9 100644
--- a/test/by_cases.expected.out
+++ b/test/by_cases.expected.out
@@ -17,3 +17,9 @@
 
 {"proofState": 2, "goals": ["case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
+{"sorries":
+ [{"proofState": 3, "goal": "case inl\nx : Int\nh : x < 0\n⊢ x = x"},
+  {"proofState": 4, "goal": "case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
+ "proofState": 5,
+ "goals": []}
+
diff --git a/test/by_cases.in b/test/by_cases.in
index 6fab1b6..9498c79 100644
--- a/test/by_cases.in
+++ b/test/by_cases.in
@@ -4,3 +4,5 @@
 
 {"proofState" : 1, "tactic": "case inl => rfl"}
 
+{"proofState" : 1, "tactic": "all_goals sorry"}
+