UNCHANGED
Conv.UNCHANGED : exception
Raised by a conversion to indicate that a term should remain unchanged.
When a conversion c is applied to a term t this can raise the
exception UNCHANGED to indicate that t should not be changed to
another term t'.
Since in this case we have a function raising an exception, we describe
this as failure of the function c. However it may be the intended
result (as used, for example, by ALL_CONV or TRY_CONV).
When conversions are combined using THENC or ORELSEC, raising
UNCHANGED is treated as though |- t = t were returned.
When a conversion c is used to produce an inference rule CONV_RULE c
or a tactic CONV_TAC c, and c raises UNCHANGED, the rule
CONV_RULE c or tactic CONV_TAC c succeeds, returning the theorem or
goal unchanged.
See also
Abbrev.conv, Conv.QCONV,
Conv.QCHANGED_CONV,
Conv.ALL_CONV, Conv.TRY_CONV,
Conv.CONV_RULE,
Tactic.CONV_TAC, Conv.THENC,
Conv.ORELSEC