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