\DOC subtract

\TYPE {subtract : 'a list -> 'a list -> 'a list}

\SYNOPSIS
Computes the set-theoretic difference of two `sets'.

\KEYWORDS
list, set.

\DESCRIBE
{subtract l1 l2} returns a list consisting of those elements of {l1} that do
not appear in {l2}. If both lists are initially free of repetitions, this can
be considered a set difference operation.

\FAILURE
Never fails.

\EXAMPLE
{
  # subtract [1;2;3] [3;5;4;1];;
  val it : int list = [2]
  # subtract [1;2;4;1] [4;5];;
  val it : int list = [1; 2; 1]
}

\SEEALSO
setify, set_eq, union, intersect.

\ENDDOC

{"subset_name": "curated", "file": "formal/hol/Help/subtract.doc"}