Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 541:429e95d23b26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Typo fix
author Adam Chlipala <adam@chlipala.net>
date Sat, 19 Sep 2015 07:44:42 -0400
parents d65e9c1c9041
children 81d63d9c1cc5
comparison
equal deleted inserted replaced
540:582bf8d4ce51 541:429e95d23b26
942 forall n : nat_tree, P n 942 forall n : nat_tree, P n
943 ]] 943 ]]
944 944
945 There is no command like [Scheme] that will implement an improved principle for us. In general, it takes creativity to figure out _good_ ways to incorporate nested uses of different type families. Now that we know how to implement induction principles manually, we are in a position to apply just such creativity to this problem. 945 There is no command like [Scheme] that will implement an improved principle for us. In general, it takes creativity to figure out _good_ ways to incorporate nested uses of different type families. Now that we know how to implement induction principles manually, we are in a position to apply just such creativity to this problem.
946 946
947 Many induction principles for types with nested used of [list] could benefit from a unified predicate capturing the idea that some property holds of every element in a list. By defining this generic predicate once, we facilitate reuse of library theorems about it. (Here, we are actually duplicating the standard library's [Forall] predicate, with a different implementation, for didactic purposes.) *) 947 Many induction principles for types with nested uses of [list] could benefit from a unified predicate capturing the idea that some property holds of every element in a list. By defining this generic predicate once, we facilitate reuse of library theorems about it. (Here, we are actually duplicating the standard library's [Forall] predicate, with a different implementation, for didactic purposes.) *)
948 948
949 Section All. 949 Section All.
950 Variable T : Set. 950 Variable T : Set.
951 Variable P : T -> Prop. 951 Variable P : T -> Prop.
952 952