gen_find_terms
HolKernel.gen_find_terms : (term list * term -> 'a option) -> term -> 'a list
Maps a partial function over sub-terms of a term.
A call to gen_find_terms f t returns a list of values derived from
sub-terms of term t. The values are those generated by the function
f when it returns SOME v. The function f is successively passed
sub-terms of t starting with t itself and then proceeding in a
top-down, left-to-right traversal. The list of results returned in the
reverse of this order (but the fact that the traversal is done in the
described order is observable if f has side effects).
The additional list of terms passed to the function f is the list of
bound variables "governing" the sub-term in question, with the innermost
bound variable first in the list.
Failure
A call to gen_find_terms f t will fail if f fails when applied to
any of the sub-terms of t.
Example
> gen_find_terms (fn x => SOME x) ``SUC x``;
val it = [([], “x”), ([], “SUC”), ([], “SUC x”)]: (term list * term) list
> gen_find_terms
(fn (bvs,t) => if null bvs andalso
(is_var t orelse numSyntax.is_numeral t)
then
Lib.total (match_term ``x:num``) t
else NONE)
``SUC z + (\y. y) 5``;
val it =
[([{redex = “x”, residue = “5”}], []),
([{redex = “x”, residue = “z”}], [])]:
((term, term) Term.subst * (hol_type, hol_type) Term.subst) list
See also
HolKernel.bvk_find_term,
HolKernel.find_term,
HolKernel.gen_find_term