Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 202:8caa3b3f8fc0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Feedback from Peter Gammie
author Adam Chlipala <adamc@hcoop.net>
date Sat, 03 Jan 2009 19:57:02 -0500
parents a2b14ba218a7
children f05514cc6c0d
comparison
equal deleted inserted replaced
201:a2b14ba218a7 202:8caa3b3f8fc0
447 Implicit Arguments Nil [T]. 447 Implicit Arguments Nil [T].
448 (* end hide *) 448 (* end hide *)
449 449
450 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. *) 450 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. *)
451 451
452 Check list. 452 Print list.
453 (** [[ 453 (** [[
454 454
455 list 455
456 : Set -> Set 456 Inductive list (T : Set) : Set :=
457 ]] *) 457 Nil : list T | Cons : T -> list T -> list Tlist
458 458 ]]
459 Check Cons. 459
460 (** [[ 460 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. *)
461
462 Cons
463 : forall T : Set, T -> list T -> list T
464 ]] *)
465 461
466 Check length. 462 Check length.
467 (** [[ 463 (** [[
468 464
469 length 465 length
470 : forall T : Set, list T -> nat 466 : forall T : Set, list T -> nat
471 ]] 467 ]]
472 468
473 The extra parameter [T] is treated as a new argument to the induction principle, too. *) 469 The parameter [T] is treated as a new argument to the induction principle, too. *)
474 470
475 Check list_ind. 471 Check list_ind.
476 (** [[ 472 (** [[
477 473
478 list_ind 474 list_ind
1091 H : true = false 1087 H : true = false
1092 ============================ 1088 ============================
1093 f false 1089 f false
1094 ]] 1090 ]]
1095 1091
1096 Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite. *) 1092 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. *)
1097 1093
1098 rewrite <- H. 1094 rewrite <- H.
1099 (** [[ 1095 (** [[
1100 1096
1101 H : true = false 1097 H : true = false