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