Lib.delta

delta_pair : ('a -> 'a delta) ->
             ('b -> 'b delta) ->
             'a * 'b -> ('a * 'b) delta

STRUCTURE: Lib
SYNOPSIS: Apply two functions to the projections of a pair, sharing as much structure as possible.
DESCRIPTION: An application delta_pair f g (x,y) applies f to x and g to y. If f x equals g y equals SAME, then SAME is returned. Otherwise DIFF (p1,p2) is returned, where p1 is x if f x equals SAME; otherwise p1 is f x. Similarly, p2 is y if g y equals SAME; otherwise p2 is g y.
FAILURE: If f x raises e, then delta_pair f g (x,y) raises e.
If g y raises e, then delta_pair f g (x,y) raises e.
EXAMPLE: See the example in the documentation for delta_apply.
SEEALSO: delta, delta_apply, delta_pair

HOL Kananaskis-14