Nuprl Definition : bm_inDomain
bm_inDomain(compare;m;x) ==
binary_map_ind(m;ff;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 tt
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,
bfalse: ff,
btrue: tt,
apply: f a,
natural_number: $n
FDL editor aliases :
bm_inDomain
Latex:
bm\_inDomain(compare;m;x) ==
binary\_map\_ind(m;ff;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 tt
fi )
Date html generated:
2016_05_17-PM-01_41_34
Last ObjectModification:
2012_08_27-AM-10_06_37
Theory : binary-map
Home
Index