(kernel)
| 157 | |
| 158 | |
| 159 | def test_goal_try_define_with_value(kernel): |
| 160 | state = kernel.goal_create("∀ n : Nat, n + 0 = n") |
| 161 | res = state.try_define("h", "(0 : Nat)") |
| 162 | assert res.status in {"success", "invalidAction", "failure", "parseError"} |
| 163 | |
| 164 | |
| 165 | def test_goal_try_draft_with_sorry(kernel): |
nothing calls this directly
no test coverage detected