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: Oct 13 2024 at 01:02 UTC