Nuprl Definition : bm_insert_if_not

Nuprl Definition : bm_insert_if_not_in

bm_insert_if_not_in(compare;m;x;v) ==
binary_map_ind(m;bm_T(x;v;1;bm_E();bm_E());key,value,cnt,left,right,recL,recR.let c ←─ compare key x

                                                                                in if 0 <z c

                                                                                     then bm_T'(key;value;recL;right)

                                                                                if c <z 0

                                                                                  then bm_T'(key;value;left;recR)

                                                                                else bm_T(key;value;cnt;left;right)

                                                                                fi )

Definitions occuring in Statement : 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_T: bm_T(key;value;cnt;left;right), bm_E: bm_E(), callbyvalueall: callbyvalueall, ifthenelse: if b then t else f fi , lt_int: i <z j, apply: f a, natural_number: $n
FDL editor aliases : bm_insert_if_not_in
bm\_insert\_if\_not\_in(compare;m;x;v) == binary\_map\_ind(m;bm\_T(x;v;1;bm\_E();bm\_E());key,value,cnt,left,right,recL,recR.let c \mleftarrow{}{} compare key x in if 0 <z c then ... if c <z 0 then ... else ... fi ) Date html generated: 2015_07_17-AM-08_19_43 Last ObjectModification: 2012_12_24-PM-00_37_02 Home Index