Re: [O] Literate programming of interactive proofs?

2012-11-19 Thread Alan Schmitt
Eric Schulte writes: > If you do end up writing any level of support for Coq code blocks please > consider contributing it to Org-mode. Thanks a lot for these suggestions. I'll explore these options, and will report back when I get something working. Alan

Re: [O] Literate programming of interactive proofs?

2012-11-16 Thread Eric Schulte
Alan Schmitt writes: > Hello, > > I want to use org-mode to write a paper about a development in Coq. Coq > is an interactive proof system, which can be run (among other ways) > interactively through emacs. The interactive part is very important, as > doing or maintaining proofs often requires ex

[O] Literate programming of interactive proofs?

2012-11-15 Thread Alan Schmitt
Hello, I want to use org-mode to write a paper about a development in Coq. Coq is an interactive proof system, which can be run (among other ways) interactively through emacs. The interactive part is very important, as doing or maintaining proofs often requires exploring many different direction.