TRY_CONV
Conv.TRY_CONV : conv -> conv
Attempts to apply a conversion; applies identity conversion in case of failure.
TRY_CONV c t attempts to apply the conversion c to the term t; if
this fails, then the identity conversion is applied instead. That is, if
c is a conversion that maps a term t to the theorem |- t = t',
then the conversion TRY_CONV c also maps t to |- t = t'. But if
c fails when applied to t, then TRY_CONV c t raises the
UNCHANGED exception (which is understood to mean the instance of
reflexivity, |- t = t). If c applied to t raises the UNCHANGED
exception, then so too does TRY_CONV c t.
Failure
Never fails, except that the UNCHANGED exception can be raised.
See also
Conv.UNCHANGED,
Conv.QCHANGED_CONV,
Conv.ALL_CONV, Conv.QCONV