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"} +