Nuprl Definition : bm_try_remove
bm_try_remove(compare;m;x) ==
binary_map_ind(m;<bm_E(), inr ⋅ >;key,value,cnt,left,right,recL,recR.eval c = compare key x in
if 0 <z c
then let left',v = recL
in <bm_T'(key;value;left';right), v>
if c <z 0
then let right',v = recR
in <bm_T'(key;value;left;right'), v>
else <bm_delete'(left;right), inl value>
fi )
Definitions occuring in Statement :
bm_delete': bm_delete'(m1;m2),
bm_T': bm_T'(k;v;m1;m2),
binary_map_ind: binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]),
bm_E: bm_E(),
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
it: ⋅,
apply: f a,
spread: spread def,
pair: <a, b>,
inr: inr x ,
inl: inl x,
natural_number: $n
FDL editor aliases :
bm_try_remove
bm\_try\_remove(compare;m;x) ==
binary\_map\_ind(m;<bm\_E(), inr \mcdot{} >key,value,cnt,left,right,recL,recR.eval c = compare key x in
if 0 <z c
then let left',v = recL
in <bm\_T'(key;value;left';right), v>
if c <z 0
then let right',v = recR
in <bm\_T'(key;value;left;right'), v>
else <bm\_delete'(left;right), inl value>
fi )
Date html generated:
2015_07_17-AM-08_20_00
Last ObjectModification:
2013_01_04-PM-00_02_51
Home
Index