Jakob Israelsen (Sep 30 2022 at 09:23): 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?
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.
Jakob Israelsen (Sep 30 2022 at 09:28):Ah, that makes sense, thank you!
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: Apr 18 2024 at 22:02 UTC