op_mem

Lib.op_mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool

Tests whether a list contains a certain element.

An invocation op_mem eq x [x1,...,xn] returns true if, for some xi in the list, eq xi x evaluates to true. Otherwise it returns false.

Failure

Only fails if an application of eq fails.

Example

- op_mem aconv (Term `\x. x /\ y`) [T, Term `\z. z /\ y`, F];
> val it = true : bool

Comments

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

See also

Lib.mem, Lib.op_insert, Lib.tryfind, Lib.exists, Lib.all, Lib.assoc, Lib.rev_assoc, Lib.assoc1, Lib.assoc2, Lib.op_union, Lib.op_mk_set, Lib.op_U, Lib.op_intersect, Lib.op_set_diff