Nuprl Definition : bm_lookup
bm_lookup(compare;m;x) ==
binary_map_ind(m;"error";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 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,
apply: f a,
natural_number: $n,
token: "$token"
FDL editor aliases :
bm_lookup
bm\_lookup(compare;m;x) ==
binary\_map\_ind(m;"error";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 value
fi )
Date html generated:
2015_07_17-AM-08_19_51
Last ObjectModification:
2012_08_27-AM-10_25_01
Home
Index