Nuprl Definition : alpha-avoid
alpha-avoid(L;t) == alpha-rename(alist-map(VarDeq;alpha-rename-alist(t;L));t)
Definitions occuring in Statement :
alpha-rename-alist: alpha-rename-alist(t;L),
alpha-rename: alpha-rename(f;t),
var-deq: VarDeq,
alist-map: alist-map(eq;L)
Definitions occuring in definition :
alpha-rename: alpha-rename(f;t),
alist-map: alist-map(eq;L),
var-deq: VarDeq,
alpha-rename-alist: alpha-rename-alist(t;L)
FDL editor aliases :
alpha-avoid
Latex:
alpha-avoid(L;t) == alpha-rename(alist-map(VarDeq;alpha-rename-alist(t;L));t)
Date html generated:
2020_05_19-PM-09_57_20
Last ObjectModification:
2020_03_09-PM-04_09_41
Theory : terms
Home
Index