BINDER_CONV
Conv.BINDER_CONV : conv -> conv
Applies a conversion underneath a binder.
If conv N returns A |- N = P, then BINDER_CONV conv (M (\v.N))
returns A |- M (\v.N) = M (\v.P) and BINDER_CONV conv (\v.N) returns
A |- (\v.N) = (\v.P)
Failure
If conv N fails, or if v is free in A.
Example
> BINDER_CONV SYM_CONV (Term `\x. x + 0 = x`);
val it = ⊢ (λx. x + 0 = x) = (λx. x = x + 0): thm
Comments
For deeply nested quantifiers, STRIP_BINDER_CONV and
STRIP_QUANT_CONV are more efficient than iterated application of
BINDER_CONV, BINDER_CONV, or ABS_CONV.
See also
Conv.QUANT_CONV,
Conv.STRIP_QUANT_CONV,
Conv.STRIP_BINDER_CONV,
Conv.ABS_CONV