Nuprl Definition : swap
swap(i;j) == λn.if (n =z i) then j if (n =z j) then i else n fi
Wellformedness Lemmas :
swap_wf
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j)
Latex:
swap(i;j) == \mlambda{}n.if (n =\msubz{} i) then j if (n =\msubz{} j) then i else n fi
Date html generated:
2016_05_16-AM-07_29_27
Last ObjectModification:
2015_09_23-AM-09_51_17
Theory : perms_1
Home
Index