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

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 |