## Mercurial > cpdt > repo

### comparison src/InductiveTypes.v @ 488:31258618ef73

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Incorporate feedback from Nathan Collins

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Tue, 08 Jan 2013 14:38:56 -0500 |

parents | 1fd4109f7b31 |

children | 4a663981b699 |

comparison

equal
deleted
inserted
replaced

487:8bfb27cf0121 | 488:31258618ef73 |
---|---|

505 P (Nil T) -> | 505 P (Nil T) -> |

506 (forall (t : T) (l : list T), P l -> P (Cons t l)) -> | 506 (forall (t : T) (l : list T), P l -> P (Cons t l)) -> |

507 forall l : list T, P l | 507 forall l : list T, P l |

508 ]] | 508 ]] |

509 | 509 |

510 Thus, even though we just saw that [T] is added as an extra argument to the constructor [Cons], the inductive case in the type of [list_ind] (i.e., the third line of the type) includes no quantifier for [T], even though all of the other arguments are quantified explicitly. Parameters in other inductive definitions are treated similarly in stating induction principles. *) | 510 Thus, despite a very real sense in which the type [T] is an argument to the constructor [Cons], the inductive case in the type of [list_ind] (i.e., the third line of the type) includes no quantifier for [T], even though all of the other arguments are quantified explicitly. Parameters in other inductive definitions are treated similarly in stating induction principles. *) |

511 | 511 |

512 | 512 |

513 (** * Mutually Inductive Types *) | 513 (** * Mutually Inductive Types *) |

514 | 514 |

515 (** We can define inductive types that refer to each other: *) | 515 (** We can define inductive types that refer to each other: *) |