Nuprl Definition : bm

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

Latex:
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: 2016_05_17-PM-01_41_41 Last ObjectModification: 2012_08_27-AM-10_14_13 Theory : binary-map Home Index