Mercurial > cpdt > repo

comparison src/Generic.v @ 428:b027b39606ed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through Generic, to incorporate new coqdoc features
author Adam Chlipala <adam@chlipala.net>
date Thu, 26 Jul 2012 11:22:46 -0400
parents 7c2167c3fbb2
children 8077352044b2
comparison
equal deleted inserted replaced
427:5e6b76ca14de 428:b027b39606ed
358 end 358 end
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 *)
364 Definition append' := append.
365 (* end hide *)
366
363 (** 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. *) 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. *)
364 368
365 369
366 (** ** Mapping *) 370 (** ** Mapping *)
367 371
639 ]] 643 ]]
640 644
641 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.*) 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.*)
642 646
643 induction r; crush. 647 induction r; crush.
648
649 (* begin hide *)
650 Definition pred' := pred.
651 (* end hide *)
644 652
645 (** 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). 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).
646 [[ 654 [[
647 H : forall i : fin (S n), 655 H : forall i : fin (S n),
648 fx T 656 fx T