----------------------------------------------------------------------
find_terms                                                 (HolKernel)
----------------------------------------------------------------------
find_terms : (term -> bool) -> term -> term list

SYNOPSIS
Traverses a term, returning a list of sub-terms satisfying a predicate.

KEYWORDS
Term.

DESCRIBE
A call to {find_terms P t} returns a list of sub-terms of {t} that
satisfy {P}.  The resulting list is ordered as if the traversal had
been bottom-up and right-to-left (i.e., the rands of combs visited
before their rators).  The term {t} is itself considered a possible
sub-term of {t}.

FAILURE
Only fails if the predicate fails on one of the term’s sub-terms.

EXAMPLE

- find_terms (fn _ => true) ``x + y``;
> val it = [``y``, ``x``, ``$+``, ``$+ x``, ``x + y``]

- find_terms Literal.is_numeral ``x + y``;
> val it = [] : term list

- find_terms Literal.is_numeral ``1 + x + 2 + y``;
> val it = [``2``, ``1``] : term list


SEEALSO
HolKernel.bvk_find_term, HolKernel.find_term.

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