Mercurial > repo
changeset 369:b30df78e892e
<elliott> pastelogs proofgeneral
author | HackBot |
---|---|
date | Mon, 30 Apr 2012 23:15:13 +0000 |
parents | 1e9ba72e22bc |
children | de47fb2aac40 |
files | paste/paste.16467 |
diffstat | 1 files changed, 8 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paste/paste.16467 Mon Apr 30 23:15:13 2012 +0000 @@ -0,0 +1,8 @@ +2010-08-21.txt:00:24:22: <botte> coq's syntax is better than agda for people who actually use it. interactive development is possible with Proof General; much nicer than Agda's mode. Proving things in Agda is almost impossible; it is not developed for that at all, while Coq is built around it. ProofGeneral makes it even nicer. +2010-08-21.txt:17:24:29: <alise> use proofgeneral with electric mode and three window mode +2010-08-21.txt:17:25:05: <alise> with proofgeneral electric three-window you have one window for your file +2010-08-21.txt:17:26:54: <Phantom_Hoover> alise, I haven't tried Proofgeneral yet, though. +2010-08-22.txt:21:59:25: <Vonlebio> OK, why has Proofgeneral's indentation behaviour changed all of a sudden? +2010-11-28.txt:17:45:30: * Phantom_Hoover decides to reduce his confusion with ProofGeneral steppery. +2011-04-07.txt:20:07:30: <elliott> proofgeneral's interface to the toplevel. +2011-04-07.txt:20:08:19: <elliott> augur: turn on three window mode and electric terminator in proofgeneral