Hi new Zulip user here :) I am not sure if this is the correct format and place to ask questions but here I am :)
I am wondering how to let my customized plugin command "start a new proof/goal"?
My current way of developing plugins is to translate my command into vernac_expr and invoke Vernacinterp.interp. This works fine and satisfies most of my needs, but when I use the same idea to translate my command into VernacStartTheoremProof (which should correspond to using Theorem command), the interp function finished successfully but my VsCoq interface didn't enter the proof mode (as far as it looks like, I am not sure if there is any display error by VsCoq; I also tried to input Qed but it does error with the message "No Focused Proof....")
Looking forward to any suggestions! I guess there are some plugins that can enter the proof mode but I don't know where to find them :) Great Thanks!
you need to classify as vtstartproof in your mlg
something like this https://github.com/coq/coq/blob/58465d29ec8154af22e8e9a394502288a72b71e7/plugins/ltac/g_obligations.mlg#L86-L90
(the CLASSIFIED BY part)
Gaëtan Gilbert said:
something like this https://github.com/coq/coq/blob/58465d29ec8154af22e8e9a394502288a72b71e7/plugins/ltac/g_obligations.mlg#L86-L90
Thanks for the help! I will try to transplant this example into mine :)
Last updated: Oct 13 2024 at 01:02 UTC