Mercurial > repo

view paste/paste.16467 @ 11293:a7899ef2d7b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
<wob_jonas> learn Aristotle said that every illness can be cured by balancing the four vitreous humors, and everyone believed him for two thousand years, even though people still died of illnesses. It wasn\'t until the 20th century that Szent-Gy\xc3\xb6rgyi Albert realized that Aristotle didn\'t find fifth kind of vitreous humor, vitamin C, because the Greek alphabet
author HackBot
date Mon, 01 Jan 2018 17:57:43 +0000
parents b30df78e892e
children
line wrap: on
line source

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