diff src/InductiveTypes.v @ 202:8caa3b3f8fc0

Feedback from Peter Gammie
author Adam Chlipala <adamc@hcoop.net>
date Sat, 03 Jan 2009 19:57:02 -0500
parents a2b14ba218a7
children f05514cc6c0d
line wrap: on
line diff
--- a/src/InductiveTypes.v	Fri Jan 02 09:09:35 2009 -0500
+++ b/src/InductiveTypes.v	Sat Jan 03 19:57:02 2009 -0500
@@ -449,19 +449,15 @@
 
 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. *)
 
-Check list.
+Print list.
 (** [[
 
-list
-     : Set -> Set
-]] *)
 
-Check Cons.
-(** [[
+Inductive list (T : Set) : Set :=
+    Nil : list T | Cons : T -> list T -> list Tlist
+]]
 
-Cons
-     : forall T : Set, T -> list T -> list T
-]] *)
+The final definition is the same as what we wrote manually before.  The other elements of the section are altered similarly, turning out exactly as they were before, though we managed to write their definitions more succinctly. *)
 
 Check length.
 (** [[
@@ -470,7 +466,7 @@
      : forall T : Set, list T -> nat
 ]]
 
-The extra parameter [T] is treated as a new argument to the induction principle, too. *)
+The parameter [T] is treated as a new argument to the induction principle, too. *)
 
 Check list_ind.
 (** [[
@@ -1093,7 +1089,7 @@
    f false
 ]]
 
-Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite. *)
+Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite, using the notation [<-] to request to replace the righthand side the equality with the lefthand side. *)
 
   rewrite <- H.
 (** [[