annotate paste/paste.16467 @ 10881:18545542ce6f
<wob_jonas> `` perl -we \'open$I,"<",$ARGV[0]or die;local$/;$s=<$I>;$s=~s/(.*;) d.*/$1 discrete, discreet./s;print substr($s,200),"||";open$O,">",$ARGV[0];print$O $s;\' "wisdom/b_jonas can\'t spell"
author |
HackBot |
date |
Wed, 10 May 2017 23:53:46 +0000 |
parents |
b30df78e892e |
children |
|
rev |
line source |
369
|
1 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.
|
|
2 2010-08-21.txt:17:24:29: <alise> use proofgeneral with electric mode and three window mode
|
|
3 2010-08-21.txt:17:25:05: <alise> with proofgeneral electric three-window you have one window for your file
|
|
4 2010-08-21.txt:17:26:54: <Phantom_Hoover> alise, I haven't tried Proofgeneral yet, though.
|
|
5 2010-08-22.txt:21:59:25: <Vonlebio> OK, why has Proofgeneral's indentation behaviour changed all of a sudden?
|
|
6 2010-11-28.txt:17:45:30: * Phantom_Hoover decides to reduce his confusion with ProofGeneral steppery.
|
|
7 2011-04-07.txt:20:07:30: <elliott> proofgeneral's interface to the toplevel.
|
|
8 2011-04-07.txt:20:08:19: <elliott> augur: turn on three window mode and electric terminator in proofgeneral
|