- I like to use Emacs to run ProofGeneral/Coq-mode, because the interactive tool for proving is great.
- I like to use Emacs to run Org-mode, because is a very simple way to write a presentation that I can edit text while doing it.
Can I have both things at same time and at the same buffer?
My propose in doing this is to have a good way to make a presentation about Coq where I can hide/fold bullets and execute Coq code. What I mean by "execute Coq code" is to use the interactive tool for checking the proof.
I think that would be a nice way to make a presentation about Coq. But if you think that this is not a good idea, I'm open mind for nice way to give a presentation about Coq.
Now, the problem is how to do it! I'm quite newbie to all the tools related to it and don't even know if is possible.