1\DOC BINDER_CONV 2 3\TYPE {BINDER_CONV : conv -> conv} 4 5\SYNOPSIS 6Applies a conversion underneath a binder. 7 8\KEYWORDS 9conversion, quantifier. 10 11\DESCRIBE 12If {conv N} returns {A |- N = P}, then {BINDER_CONV conv (M (\v.N))} returns 13{A |- M (\v.N) = M (\v.P)} and {BINDER_CONV conv (\v.N)} returns 14{A |- (\v.N) = (\v.P)} 15 16\FAILURE 17If {conv N} fails, or if {v} is free in {A}. 18 19\EXAMPLE 20{ 21- BINDER_CONV SYM_CONV (Term `\x. x + 0 = x`); 22> val it = |- (\x. x + 0 = x) = \x. x = x + 0 : thm 23} 24 25\COMMENTS 26For deeply nested quantifiers, {STRIP_BINDER_CONV} and 27{STRIP_QUANT_CONV} are more efficient than iterated application of 28{BINDER_CONV}, {BINDER_CONV}, or {ABS_CONV}. 29 30\SEEALSO 31Conv.QUANT_CONV, Conv.STRIP_QUANT_CONV, Conv.STRIP_BINDER_CONV, Conv.ABS_CONV. 32 33\ENDDOC 34