Stream: Proof General users

Topic: Extracting goal to Lemma


view this post on Zulip Jakob Israelsen (Sep 30 2022 at 09:23):

I am fairly new to Emacs in general, and Proof General specifically. I stumbled upon a stackoverflow answer (https://stackoverflow.com/a/41838593) that mentions a shortcut fro extracting a goal into a lemma, but I cannot figure out how to use it. The shortcut should be C-c C-a C-x, (which I understand to be holding control down while typing cax), but nothing happens to the proof I am looking at. Any suggestions for what I could be doing wrong?

view this post on Zulip Karl Palmskog (Sep 30 2022 at 09:24):

did you install Company-Coq? https://github.com/cpitclaudel/company-coq

I think this functionality is only available when you have both Proof General and Company-Coq installed.

view this post on Zulip Jakob Israelsen (Sep 30 2022 at 09:28):

Ah, that makes sense, thank you!

view this post on Zulip Pierre Courtieu (Oct 03 2022 at 11:48):

It is indeed a company-coq feature. You probably want to try the tutorial once you install it: M-x company-coq-tutorial.


Last updated: Feb 06 2023 at 06:29 UTC