Nuprl Definition : swap-names

swap-names(z1;z2) ==  λx.if eq-cname(x;z1) then z2 if eq-cname(x;z2) then z1 else x fi 


Definitions occuring in Statement :  eq-cname: eq-cname(x;y),  ifthenelse: if b then t else f fi ,  lambda: λx.A[x]
Definitions occuring in definition :  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq-cname: eq-cname(x;y)
FDL editor aliases :  swap-names
Latex:
swap-names(z1;z2)  ==    \mlambda{}x.if  eq-cname(x;z1)  then  z2  if  eq-cname(x;z2)  then  z1  else  x  fi 


Date html generated: 2016_05_20-AM-09_34_12
Last ObjectModification: 2015_09_23-AM-09_29_40

Theory : cubical!sets


Home Index