Nuprl Definition : permute-to-front
permute-to-front(L;idxs) ==
(L o λi.filter(λi.int-list-member(i;idxs);upto(||L||)) @ filter(λi.(¬bint-list-member(i;idxs));upto(||L||))[i])
Definitions occuring in Statement :
int-list-member: int-list-member(i;xs),
permute_list: (L o f),
upto: upto(n),
select: L[n],
length: ||as||,
filter: filter(P;l),
append: as @ bs,
bnot: ¬bb,
lambda: λx.A[x]
Definitions occuring in definition :
permute_list: (L o f),
select: L[n],
append: as @ bs,
filter: filter(P;l),
lambda: λx.A[x],
bnot: ¬bb,
int-list-member: int-list-member(i;xs),
upto: upto(n),
length: ||as||
FDL editor aliases :
permute-to-front
Latex:
permute-to-front(L;idxs) ==
(L o \mlambda{}i.filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))
@ filter(\mlambda{}i.(\mneg{}\msubb{}int-list-member(i;idxs));upto(||L||))[i])
Date html generated:
2016_05_15-PM-04_23_08
Last ObjectModification:
2015_09_23-AM-07_48_10
Theory : general
Home
Index