1129199Scognet\DOC GEN_PALPHA_CONV 2137550Scognet 3142591Scognet\TYPE {GEN_PALPHA_CONV : term -> conv} 4135671Scognet 5161105Scognet\LIBRARY 6147115Scognetpair 7153277Scognet 8135671Scognet\KEYWORDS 9135671Scognetconversion, alpha. 10135671Scognet 11170583Scognet\SYNOPSIS 12135671ScognetRenames the bound pair of a paired abstraction, quantified term, 13170583Scognetor other binder. 14164427Ssam 15166820Scognet\DESCRIBE 16135671ScognetThe conversion {GEN_PALPHA_CONV} provides alpha conversion for lambda 17135671Scognetabstractions of the form {\p.t}, quantified terms of the forms {!p.t}, 18166820Scognet{?p.t} or {?!p.t}, and epsilon terms of the form {@p.t}. 19158531Scognet 20158531ScognetThe renaming of pairs is as described for {PALPHA_CONV}. 21135671Scognet 22135671Scognet\FAILURE 23157567Scognet{GEN_PALPHA_CONV q tm} fails if {q} is not a variable, 24159322Scognetor if {tm} does not have one of the required forms. 25165784Sticso{GEN_ALPHA_CONV q tm} also fails if {tm} does have one of these forms, 26160360Simpbut types of the variables {p} and {q} differ. 27160360Simp 28\SEEALSO 29Drule.GEN_ALPHA_CONV, PairRules.PALPHA, PairRules.PALPHA_CONV. 30\ENDDOC 31