bvk_find_term : (term list * term -> bool) -> (term -> 'a) -> term -> 'a option
The search order is top-down, left-to-right (i.e., rators of combs are examined before rands).
As with find_term, P should be total. In addition, P is given not just the sub-term of interest, but also the stack of bound variables that have scope over the sub-term, with the innermost bound variables appearing earlier in the list.
- val find = bvk_find_term (equal ``:num`` o type_of o #2) reduceLib.RED_CONV; > val find = fn : term -> thm option - find ``SUC n``; > val it = NONE : thm option - find ``2 * 3 + SUC n``; > val it = SOME |- 2 * 3 = 6 : thm option - find ``SUC n + 2 * 3``; > val it = SOME |- 2 * 3 = 6 : thm option - find ``2 + 1 + SUC n + 2 * 3``; > val it = SOME |- 2 + 1 = 3 : thm option