Nuprl Definition : index-split

index-split(L;idxs) ==
  let n = ||filter(λi.int-list-member(i;idxs);upto(||L||))|| in
   let L' = permute-to-front(L;idxs) in
   <firstn(n;L'), nth_tl(n;L')>


Definitions occuring in Statement :  permute-to-front: permute-to-front(L;idxs),  int-list-member: int-list-member(i;xs),  upto: upto(n),  firstn: firstn(n;as),  length: ||as||,  filter: filter(P;l),  nth_tl: nth_tl(n;as),  let: let,  lambda: λx.A[x],  pair: <a, b>
Definitions occuring in definition :  filter: filter(P;l),  lambda: λx.A[x],  int-list-member: int-list-member(i;xs),  upto: upto(n),  length: ||as||,  let: let,  permute-to-front: permute-to-front(L;idxs),  pair: <a, b>,  firstn: firstn(n;as),  nth_tl: nth_tl(n;as)
FDL editor aliases :  index-split
Latex:
index-split(L;idxs)  ==
    let  n  =  ||filter(\mlambda{}i.int-list-member(i;idxs);upto(||L||))||  in
      let  L'  =  permute-to-front(L;idxs)  in
      <firstn(n;L'),  nth\_tl(n;L')>


Date html generated: 2016_05_15-PM-04_24_28
Last ObjectModification: 2015_09_23-AM-07_48_20

Theory : general


Home Index