op_mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool
STRUCTURE
Lib
LIBRARY
Lib
SYNOPSIS
Tests whether a list contains a certain element.
DESCRIPTION
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.
SEEALSO
mem, op_insert, tryfind, exists, all, assoc, rev_assoc, assoc1, assoc2, op_union, op_mk_set, op_U, op_intersect, op_set_diff
HOL  Kananaskis-13