----------------------------------------------------------------------
find_term                                                  (HolKernel)
----------------------------------------------------------------------
find_term : (term -> bool) -> term -> term

SYNOPSIS
Finds a sub-term satisfying a predicate.

KEYWORDS
Term.

DESCRIBE
A call to {find_term P t} returns a sub-term of {t} that satisfies the
predicate {P} if there is one.  Otherwise it raises a {HOL_ERR}
exception.  The search is done in a top-down, left-to-right order
(i.e., rators of combs are examined before rands).

FAILURE
Fails if the predicate fails when applied to any of the sub-terms of the term argument.  Also fails if there is no sub-term satisfying the predicate.

EXAMPLE

- find_term Literal.is_numeral ``2 + x + 3``;
> val it = ``2`` : term

- find_term Literal.is_numeral ``x + y``;
Exception HOL_ERR {...}


SEEALSO
HolKernel.bvk_find_term, HolKernel.find_terms.

----------------------------------------------------------------------