find_term
HolKernel.find_term : (term -> bool) -> term -> term
Finds a sub-term satisfying a predicate.
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 at HolKernel.find_term: raised