----------------------------------------------------------------------
PATH_CONV                                                       (Conv)
----------------------------------------------------------------------
PATH_CONV : string -> conv -> conv

SYNOPSIS
Applies a conversion to the subterm indicated by a path string.

KEYWORDS
rewriting

DESCRIBE
A call to {PATH_CONV p c} returns a new conversion that applies {c} to
the subterm of a term identified by the path string {p}. This path
string is interpreted as a sequence of direction indications: {"a"}:
take the body of an abstraction; {"b"}: take the body of an abstraction
or binder (such as universal or existential quantification); {"l"}: take
the left (rator) path in an application; {"r"}: take the right (rand)
path in an application.

FAILURE
The call to the path string and conversion fails if the provided string includes characters other than {a}, {b}, {l} or {r}.  When applied to a term the resulting conversion will fail if the path is not meaningful or if the conversion itself fails on the indicated subterm.

EXAMPLE

> PATH_CONV "lrr" numLib.REDUCE_CONV ``(1 + 2) + (3 + 4) + (5 + 6)``;
val it = |- 1 + 2 + (3 + 4) + (5 + 6) = 1 + 2 + 7 + (5 + 6) : thm

> PATH_CONV "br" numLib.REDUCE_CONV ``!x. x > 10 + 3``;
val it = |- (!x. x > 10 + 3) <=> !x. x > 13 : thm


COMMENTS
This function provides a more concise indication of sub-conversion
application than by composing {RATOR_CONV}, {RAND_CONV} and {ABS_CONV}.

SEEALSO
Conv.ABS_CONV, Conv.BINDER_CONV, Conv.RAND_CONV, Conv.RATOR_CONV.

----------------------------------------------------------------------