Mercurial > cpdt > repo
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. |