delta_map : ('a -> 'a delta) -> 'a list -> 'a list delta
STRUCTURE
SYNOPSIS
Apply a function to a list, sharing as much structure as possible.
DESCRIPTION
An application delta_map f list applies f to each member [x1,...,xn] of list. If all applications of f return SAME, then delta_map f list returns SAME. Otherwise, DIFF [y1,...,yn] is returned. If f xi yielded SAME, then yi is xi. Otherwise, f xi equals DIFF yi.
FAILURE
If some application of f xi raises e, then delta_map f list raises e.
EXAMPLE
See the example in the documentation for delta_apply.
SEEALSO
HOL  Kananaskis-10