Nuprl Definition : bm

Nuprl Definition : bm_remove

bm_remove(compare;m;x) ==
binary_map_ind(m;"error";key,value,cnt,left,right,recL,recR.let 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), 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]), callbyvalueall: callbyvalueall, ifthenelse: if b then t else f fi , lt_int: i <z j, apply: f a, spread: spread def, pair: <a, b>, natural_number: $n, token: "$token"
FDL editor aliases : bm_remove
bm\_remove(compare;m;x) == binary\_map\_ind(m;"error";key,value,cnt,left,right,recL,recR.let c \mleftarrow{}{} compare key x in if 0 <z c then let left',v = recL in <bm\_T'(key;value;...;...) , v > if c <z 0 then let right',v = recR in <bm\_T'(key;value;left;...) , v > else <bm\_delete'(left;right), value> fi ) Date html generated: 2015_07_17-AM-08_20_03 Last ObjectModification: 2012_08_27-AM-10_41_21 Home Index