equal
deleted
inserted
replaced
400 |
400 |
401 x |> f f #> g |
401 x |> f f #> g |
402 (x, y) |-> f f #-> g |
402 (x, y) |-> f f #-> g |
403 |
403 |
404 * Pure/library.ML: canonical list combinators fold, fold_rev, and |
404 * Pure/library.ML: canonical list combinators fold, fold_rev, and |
405 fold_yield support linear functional transformations and nesting. For |
405 fold_map support linear functional transformations and nesting. For |
406 example: |
406 example: |
407 |
407 |
408 fold f [x1, ..., xN] y = |
408 fold f [x1, ..., xN] y = |
409 y |> f x1 |> ... |> f xN |
409 y |> f x1 |> ... |> f xN |
410 |
410 |