Nuprl Definition : bm_try

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

Latex:
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: 2016_05_17-PM-01_42_06 Last ObjectModification: 2013_01_04-PM-00_02_51 Theory : binary-map Home Index