PATH_CONV : string -> conv -> conv
Applies a conversion to the subterm indicated by a path string.
The call PATH_CONV p cnv gives a new conversion that applies cnv to the
subterm of a term identified by the path string p. This path string is
interpreted as a sequence of direction indications:
- "b": take the body of an abstraction
- "l": take the left (rator) path in an application
- "r": take the right (rand) path in an application
- FAILURE CONDITIONS
The basic call to the path string and conversion never fails, but when applied
to the term it may, if the path is not meaningful or if the conversion itself
fails on the indicated subterm.
More concise indication of sub-conversion application than by composing
RATOR_CONV, RAND_CONV and ABS_CONV.
# PATH_CONV "rlr" NUM_ADD_CONV `(1 + 2) + (3 + 4) + (5 + 6)`;;
val it : thm = |- (1 + 2) + (3 + 4) + 5 + 6 = (1 + 2) + 7 + 5 + 6
- SEE ALSO