1\DOC TRY_CONV
2
3\TYPE {TRY_CONV : conv -> conv}
4
5\SYNOPSIS
6Attempts to apply a conversion;
7applies identity conversion in case of failure.
8
9\KEYWORDS
10conversion, failure, unchanged.
11
12\DESCRIBE
13
14{TRY_CONV c t} attempts to apply the conversion {c} to the term {t};
15if this fails, then the identity conversion is applied instead.  That
16is, if {c} is a conversion that maps a term {t} to the theorem {|- t = t'},
17then the conversion {TRY_CONV c} also maps {t} to {|- t = t'}. But if {c}
18fails when applied to {t}, then {TRY_CONV c t} raises the {UNCHANGED}
19exception (which is understood to mean the instance of reflexivity,
20{|- t = t}).  If {c} applied to {t} raises the {UNCHANGED} exception,
21then so too does {TRY_CONV c t}.
22
23\FAILURE
24Never fails, except that the {UNCHANGED} exception can be raised.
25
26\SEEALSO
27Conv.UNCHANGED, Conv.QCHANGED_CONV, Conv.ALL_CONV, Conv.QCONV.
28\ENDDOC
29