1\DOC QCHANGED_CONV 2 3\TYPE {QCHANGED_CONV : conv -> conv} 4 5\SYNOPSIS 6Makes a conversion fail if applying it raises the {UNCHANGED} exception. 7 8\KEYWORDS 9conversional. 10 11\DESCRIBE 12If {c} is a conversion that maps a term {t} to a theorem {|- t = t'}, 13then so too is {QCHANGED_CONV c}. If {c} applied to {t} raises the 14special {UNCHANGED} exception used by conversions to indicate that 15they haven't changed an input, then {QCHANGED_CONV c} will fail, 16raising a different exception {HOL_ERR ...} when applied to {t}. 17 18The purpose of this is that some enclosing functions handle the 19{UNCHANGED} exception as though {c} had succeeded by returning 20the theorem {|- t = t}. 21 22This behaviour is similar to that of {CHANGED_CONV}, except that that 23conversion also fails if the conversion {c} returns a theorem when 24applied to {t}, and if that theorem has alpha-convertible left and 25right hand sides. 26 27\FAILURE 28{QCHANGED_CONV c t} fails (other than by raising {UNCHANGED}) 29if {c} applied {t} raises the {UNCHANGED} exception, 30or if {c} fails otherwise when applied to {t}. 31 32\USES 33{QCHANGED_CONV} can be used in places where {CHANGED_CONV} is 34appropriate, and where one knows that the conversion argument will not 35return an instance of reflexivity, or if one does not mind this 36occurring and not being trapped. Because it is no more than an 37exception handler, {QCHANGED_CONV} is very efficient. 38 39\SEEALSO 40Conv.UNCHANGED, Conv.CHANGED_CONV. 41 42\ENDDOC 43