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?
Last updated: Oct 21 2021 at 21:03 UTC