find_termsHolKernel.find_terms : (term -> bool) -> term -> term listTraverses a term, returning a list of sub-terms satisfying a predicate.
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.
Only fails if the predicate fails on one of the term’s sub-terms.
- 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