Hello
I am developping an OCaml tactic that should behave like admit
: admit the current goal, and force to finish the proof with Admitted
. I believe it is sufficient to directly use the already existing admit
tactic? If so, in which .mli
file can I find it?
Thanks!
It's Proofview.give_up
.
thanks!
Last updated: Mar 28 2024 at 19:02 UTC