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