PATH_CONV
Conv.PATH_CONV : string -> conv -> conv
Applies a conversion to the subterm indicated by a path string.
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.
See also
Conv.ABS_CONV,
Conv.BINDER_CONV,
Conv.RAND_CONV,
Conv.RATOR_CONV