1\DOC GEN_PALPHA_CONV
2
3\TYPE {GEN_PALPHA_CONV : term -> conv}
4
5\LIBRARY
6pair
7
8\KEYWORDS
9conversion, alpha.
10
11\SYNOPSIS
12Renames the bound pair of a paired abstraction, quantified term,
13or other binder.
14
15\DESCRIBE
16The conversion {GEN_PALPHA_CONV} provides alpha conversion for lambda
17abstractions of the form {\p.t}, quantified terms of the forms {!p.t},
18{?p.t} or {?!p.t}, and epsilon terms of the form {@p.t}.
19
20The renaming of pairs is as described for {PALPHA_CONV}.
21
22\FAILURE
23{GEN_PALPHA_CONV q tm} fails if {q} is not a variable,
24or if {tm} does not have one of the required forms.
25{GEN_ALPHA_CONV q tm} also fails if {tm} does have one of these forms,
26but types of the variables {p} and {q} differ.
27
28\SEEALSO
29Drule.GEN_ALPHA_CONV, PairRules.PALPHA, PairRules.PALPHA_CONV.
30\ENDDOC
31