insert ''a -> ''a list -> ''a list
STRUCTURE
SYNOPSIS
Add an element to a list if it is not already there.
DESCRIPTION
If x is already in list, then insert x list equals list. Otherwise, x becomes an element of list.
FAILURE
Never fails.
EXAMPLE
- insert 1 [3,2];
> val it = [1, 3, 2] : int list

- insert 1 it;
> val it = [1, 3, 2] : int list

COMMENTS
In some programming situations, it is convenient to implement sets by lists, in which case insert may be helpful. However, such an implementation is only suitable for small sets.

A high-performance implementation of finite sets may be found in structure HOLset.

ML equality types are used in the implementation of insert and its kin. This limits its applicability to types that allow equality. For other types, typically abstract ones, use the ‘op_’ variants.

One should not write code that depends on where the ‘list-as-set’ algorithms place elements in the list which is being considered as a set.

SEEALSO
HOL  Kananaskis-13