Nuprl Definition : flip
(i, j) == λx.if (x =z i) then j if (x =z j) then i else x fi
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)
FDL editor aliases :
flip
Latex:
(i, j) == \mlambda{}x.if (x =\msubz{} i) then j if (x =\msubz{} j) then i else x fi
Date html generated:
2016_05_14-PM-02_13_02
Last ObjectModification:
2015_09_22-PM-05_55_37
Theory : list_1
Home
Index