Nuprl Definition : bm_find

bm_find(compare;m;x) ==
  binary_map_ind(m;inr ⋅ ;key,value,cnt,left,right,recL,recR.let c ←─ compare x key
                                                             in if 0 <z c then recR
                                                             if c <z 0 then recL
                                                             else inl value
                                                             fi )


Definitions occuring in Statement :  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,  it: ⋅,  apply: f a,  inr: inr x ,  inl: inl x,  natural_number: $n
FDL editor aliases :  bm_find
bm\_find(compare;m;x)  ==
    binary\_map\_ind(m;inr  \mcdot{}  ;key,value,cnt,left,right,recL,recR.let  c  \mleftarrow{}{}  compare  x  key
                                                                                                                          in  if  0  <z  c  then  recR
                                                                                                                          if  c  <z  0  then  recL
                                                                                                                          else  inl  value
                                                                                                                          fi  )


Date html generated: 2015_07_17-AM-08_19_48
Last ObjectModification: 2012_08_27-AM-10_14_13

Home Index