## Mercurial > cpdt > repo

### diff 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 |

line wrap: on

line diff

--- a/src/InductiveTypes.v Sat Aug 15 15:59:02 2015 -0400 +++ b/src/InductiveTypes.v Sat Sep 19 07:44:42 2015 -0400 @@ -944,7 +944,7 @@ 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. -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.) *) +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.) *) Section All. Variable T : Set.