test of all_goals sorry

leanprover-community · Jan 17, 2024 · 6d83eef · 6d83eef
1 parent 7f3620b
commit 6d83eef
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git 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
@@ -4,3 +4,5 @@
 
 {"proofState" : 1, "tactic": "case inl => rfl"}
 
+{"proofState" : 1, "tactic": "all_goals sorry"}
+
Original file line number	Diff line number	Diff line change
Expand Up		@@ -4,3 +4,5 @@

		{"proofState" : 1, "tactic": "case inl => rfl"}

		{"proofState" : 1, "tactic": "all_goals sorry"}