op_set_diff : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list

- STRUCTURE
- SYNOPSIS
- Computes the set-theoretic difference of two ‘sets’, modulo a supplied relation.
- DESCRIPTION
- op_set_diff eq l1 l2 returns a list consisting of those elements of l1 that are not eq to some element of l2.
- FAILURE
- Fails if an application of eq fails.
- EXAMPLE
- op_set_diff (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [4,5,6]; > val it = [] : int list - op_set_diff (fn x => fn y => x mod 2 = y mod 2) [1,2,3] [2,4,6,8]; > val it = [1, 3] : int list

- COMMENTS
- The order in which the elements occur in the resulting list should not be depended upon.
A high-performance implementation of finite sets may be found in structure HOLset.

- SEEALSO

HOL Kananaskis-14