diff src/InductiveTypes.v @ 32:77e1a7eda0b8

Little fixes
author Adam Chlipala <adamc@hcoop.net>
date Wed, 10 Sep 2008 12:16:54 -0400
parents 1a82839f83b7
children 8b34dade70e1
line wrap: on
line diff
--- a/src/InductiveTypes.v	Mon Sep 08 16:00:02 2008 -0400
+++ b/src/InductiveTypes.v	Wed Sep 10 12:16:54 2008 -0400
@@ -87,7 +87,7 @@
   destruct 1.
 Qed.
 
-(** Because [Empty_set] has no elements, the fact of having an element of this type implies anything.  We use [destruct 1] instead of [destruct x] in the proof because unused quantified variables are relegated to being referred to by number.  (There is a good reason for this, related to the unity of quantifiers and dependent function types.)
+(** Because [Empty_set] has no elements, the fact of having an element of this type implies anything.  We use [destruct 1] instead of [destruct x] in the proof because unused quantified variables are relegated to being referred to by number.  (There is a good reason for this, related to the unity of quantifiers and implication.  An implication is just a quantification over a proof, where the quantified variable is never used.  It generally makes more sense to refer to implication hypotheses by number than by name, and Coq treats our quantifier over an unused variable as an implication in determining the proper behavior.)
 
 We can see the induction principle that made this proof so easy: *)