1\DOC op_mem 2 3\TYPE {op_mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool} 4 5\LIBRARY 6Lib 7 8\SYNOPSIS 9Tests whether a list contains a certain element. 10 11\KEYWORDS 12list, set. 13 14\DESCRIBE 15An invocation {op_mem eq x [x1,...,xn]} returns {true} if, for 16some {xi} in the list, {eq xi x} evaluates to {true}. 17Otherwise it returns {false}. 18 19\FAILURE 20Only fails if an application of {eq} fails. 21 22\EXAMPLE 23{ 24- op_mem aconv (Term `\x. x /\ y`) [T, Term `\z. z /\ y`, F]; 25> val it = true : bool 26} 27 28 29\COMMENTS 30A high-performance implementation of finite sets may be found in 31structure {HOLset}. 32 33\SEEALSO 34Lib.mem, Lib.op_insert, Lib.tryfind, Lib.exists, Lib.all, Lib.assoc, 35Lib.rev_assoc, Lib.assoc1, Lib.assoc2, Lib.op_union, Lib.op_mk_set, Lib.op_U, 36Lib.op_intersect, Lib.op_set_diff. 37 38\ENDDOC 39