## Mercurial > cpdt > repo

### comparison src/DataStruct.v @ 534:ed829eaa91b2

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

Builds with Coq 8.5beta2

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

date | Wed, 05 Aug 2015 14:46:55 -0400 |

parents | 28c2fa8af4eb |

children |

comparison

equal
deleted
inserted
replaced

533:8921cfa2f503 | 534:ed829eaa91b2 |
---|---|

1 (* Copyright (c) 2008-2012, Adam Chlipala | 1 (* Copyright (c) 2008-2012, 2015, Adam Chlipala |

2 * | 2 * |

3 * This work is licensed under a | 3 * This work is licensed under a |

4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |

5 * Unported License. | 5 * Unported License. |

6 * The license text is available at: | 6 * The license text is available at: |

8 *) | 8 *) |

9 | 9 |

10 (* begin hide *) | 10 (* begin hide *) |

11 Require Import Arith List. | 11 Require Import Arith List. |

12 | 12 |

13 Require Import CpdtTactics. | 13 Require Import Cpdt.CpdtTactics. |

14 | 14 |

15 Set Implicit Arguments. | 15 Set Implicit Arguments. |

16 Set Asymmetric Patterns. | |

16 (* end hide *) | 17 (* end hide *) |

17 | 18 |

18 | 19 |

19 (** %\chapter{Dependent Data Structures}% *) | 20 (** %\chapter{Dependent Data Structures}% *) |

20 | 21 |

487 | 488 |

488 (** * Data Structures as Index Functions *) | 489 (** * Data Structures as Index Functions *) |

489 | 490 |

490 (** %\index{index function}%Indexed lists can be useful in defining other inductive types with constructors that take variable numbers of arguments. In this section, we consider parameterized trees with arbitrary branching factor. *) | 491 (** %\index{index function}%Indexed lists can be useful in defining other inductive types with constructors that take variable numbers of arguments. In this section, we consider parameterized trees with arbitrary branching factor. *) |

491 | 492 |

493 (* begin hide *) | |

494 Definition red_herring := O. | |

495 (* working around a bug in Coq 8.5! *) | |

496 (* end hide *) | |

497 | |

492 Section tree. | 498 Section tree. |

493 Variable A : Set. | 499 Variable A : Set. |

494 | 500 |

495 Inductive tree : Set := | 501 Inductive tree : Set := |

496 | Leaf : A -> tree | 502 | Leaf : A -> tree |

551 The automatically generated induction principle is too weak. For the [Node] case, it gives us no inductive hypothesis. We could write our own induction principle, as we did in Chapter 3, but there is an easier way, if we are willing to alter the definition of [tree]. *) | 557 The automatically generated induction principle is too weak. For the [Node] case, it gives us no inductive hypothesis. We could write our own induction principle, as we did in Chapter 3, but there is an easier way, if we are willing to alter the definition of [tree]. *) |

552 | 558 |

553 Abort. | 559 Abort. |

554 | 560 |

555 Reset tree. | 561 Reset tree. |

562 (* begin hide *) | |

563 Reset red_herring. | |

564 (* working around a bug in Coq 8.5! *) | |

565 (* end hide *) | |

556 | 566 |

557 (** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *) | 567 (** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *) |

558 | 568 |

559 Section tree. | 569 Section tree. |

560 Variable A : Set. | 570 Variable A : Set. |