Lib.insert

STRUCTURE

Lib

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

op_insert, mem, mk_set, union, U, set_diff, subtract, intersect, null_intersection, set_eq