Nuprl Definition : pv8_p2_first_unoccupied
pv8_p2_first_unoccupied() == 
ps.list_accum(a,x.if eqof(IntDeq) x a then a + 1 else a fi ;1;quicksort-int(ps))
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: x.A[x],
add: n + m,
natural_number: $n,
list_accum: list_accum(x,a.f[x; a];y;l),
int-deq: IntDeq,
eqof: eqof(d),
quicksort-int: quicksort-int(L)
FDL editor aliases :
pv8_p2_first_unoccupied
pv8_p2_first_unoccupied
pv8\_p2\_first\_unoccupied() ==
\mlambda{}ps.list\_accum(a,x.if eqof(IntDeq) x a then a + 1 else a fi ;1;quicksort-int(ps))
Date html generated:
2012_02_20-PM-07_39_33
Last ObjectModification:
2012_02_06-PM-03_07_02
Home
Index