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”]: term list
> 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 listHolKernel.bvk_find_term,
HolKernel.find_term