- 我喜欢使用 Emacs 来运行 ProofGeneral/Coq-mode，因为用于证明的交互式工具很棒。
- 我喜欢使用 Emacs 来运行 Org-mode，因为它是一种非常简单的方式来编写演示文稿，我可以在编写演示文稿的同时编辑文本。
我可以在同一个缓冲区同时拥有这两种东西吗？
我这样做的建议是有一个很好的方法来演示 Coq，我可以在其中隐藏/折叠项目符号并执行 Coq 代码。我所说的“执行 Coq 代码”是指使用交互式工具来检查证明。
我认为这将是介绍 Coq 的好方法。但是，如果您认为这不是一个好主意，我愿意接受介绍 Coq 的好方法。
现在，问题是怎么做！我对所有与之相关的工具都很陌生，甚至不知道是否可能。