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 81d63d9c1cc5
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.