comparison src/DataStruct.v @ 488:31258618ef73

Incorporate feedback from Nathan Collins
author Adam Chlipala <adam@chlipala.net>
date Tue, 08 Jan 2013 14:38:56 -0500
parents f38a3af9dd17
children 28c2fa8af4eb
comparison
equal deleted inserted replaced
487:8bfb27cf0121 488:31258618ef73
582 582
583 End tree. 583 End tree.
584 584
585 Implicit Arguments Node [A n]. 585 Implicit Arguments Node [A n].
586 586
587 (** We can redefine [sum] and [inc] for our new [tree] type. Again, it is useful to define a generic fold function first. This time, it takes in a function whose range is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *) 587 (** We can redefine [sum] and [inc] for our new [tree] type. Again, it is useful to define a generic fold function first. This time, it takes in a function whose domain is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *)
588 588
589 Section rifoldr. 589 Section rifoldr.
590 Variables A B : Set. 590 Variables A B : Set.
591 Variable f : A -> B -> B. 591 Variable f : A -> B -> B.
592 Variable i : B. 592 Variable i : B.