equal
deleted
inserted
replaced
636 |
636 |
637 text {* |
637 text {* |
638 These two functions can, for example, be used to avoid explicit @{text "lets"} for |
638 These two functions can, for example, be used to avoid explicit @{text "lets"} for |
639 intermediate values in functions that return pairs. As an example, suppose you |
639 intermediate values in functions that return pairs. As an example, suppose you |
640 want to separate a list of integers into two lists according to a |
640 want to separate a list of integers into two lists according to a |
641 treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"} |
641 threshold. If the threshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"} |
642 should be separated as @{ML "([1,2,3,4], [6,5])"}. Such a function can be |
642 should be separated as @{ML "([1,2,3,4], [6,5])"}. Such a function can be |
643 implemented as |
643 implemented as |
644 *} |
644 *} |
645 |
645 |
646 ML{*fun separate i [] = ([], []) |
646 ML{*fun separate i [] = ([], []) |