Mercurial > cpdt > repo

diff src/Large.v @ 491:da576746c3ba

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix one reported grammatical error and make my own final pass over Chapter 1
author Adam Chlipala <adam@chlipala.net>
date Fri, 18 Jan 2013 13:45:00 -0500
parents 1fd4109f7b31
children 21079e42b773
line wrap: on
line diff
--- a/src/Large.v	Tue Jan 08 16:20:01 2013 -0500
+++ b/src/Large.v	Fri Jan 18 13:45:00 2013 -0500
@@ -217,7 +217,7 @@
 Qed.
 (* end thide *)
 
-(** This style is motivated by a hard truth: one person's manual proof script is almost always mostly inscrutable to most everyone else.  I claim that step-by-step formal proofs are a poor way of conveying information.  Thus, we had might as well cut out the steps and automate as much as possible.
+(** This style is motivated by a hard truth: one person's manual proof script is almost always mostly inscrutable to most everyone else.  I claim that step-by-step formal proofs are a poor way of conveying information.  Thus, we might as well cut out the steps and automate as much as possible.
 
    What about the illustrative value of proofs?  Most informal proofs are read to convey the big ideas of proofs.  How can reading [induction e; crush] convey any big ideas?  My position is that any ideas that standard automation can find are not very big after all, and the _real_ big ideas should be expressed through lemmas that are added as hints.