Mercurial > cpdt > repo

comparison src/Generic.v @ 437:8077352044b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass over all formatting, after big pile of coqdoc changes
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 16:47:28 -0400
parents b027b39606ed
children b1fead9f68f2
comparison
equal deleted inserted replaced
436:5d5e44f905c7 437:8077352044b2
359 : forall A : Type, (A -> string) -> tree A -> string 359 : forall A : Type, (A -> string) -> tree A -> string
360 ]] 360 ]]
361 *) 361 *)
362 362
363 (* begin hide *) 363 (* begin hide *)
364 (* begin thide *)
364 Definition append' := append. 365 Definition append' := append.
366 (* end thide *)
365 (* end hide *) 367 (* end hide *)
366 368
367 (** Some of these simplified terms seem overly complex because we have turned off simplification of calls to [append], which is what uses of the [++] operator desugar to. Selective [++] simplification would combine adjacent string literals, yielding more or less the code we would write manually to implement this printing scheme. *) 369 (** Some of these simplified terms seem overly complex because we have turned off simplification of calls to [append], which is what uses of the [++] operator desugar to. Selective [++] simplification would combine adjacent string literals, yielding more or less the code we would write manually to implement this printing scheme. *)
368 370
369 371
645 At this point, it is helpful to proceed by an inner induction on the heterogeneous list [r] of recursive call results. We could arrive at a cleaner proof by breaking this step out into an explicit lemma, but here we will do the induction inline to save space.*) 647 At this point, it is helpful to proceed by an inner induction on the heterogeneous list [r] of recursive call results. We could arrive at a cleaner proof by breaking this step out into an explicit lemma, but here we will do the induction inline to save space.*)
646 648
647 induction r; crush. 649 induction r; crush.
648 650
649 (* begin hide *) 651 (* begin hide *)
652 (* begin thide *)
650 Definition pred' := pred. 653 Definition pred' := pred.
654 (* end thide *)
651 (* end hide *) 655 (* end hide *)
652 656
653 (** The base case is discharged automatically, and the inductive case looks like this, where [H] is the outer IH (for induction over [T] values) and [IHn] is the inner IH (for induction over the recursive arguments). 657 (** The base case is discharged automatically, and the inductive case looks like this, where [H] is the outer IH (for induction over [T] values) and [IHn] is the inner IH (for induction over the recursive arguments).
654 [[ 658 [[
655 H : forall i : fin (S n), 659 H : forall i : fin (S n),