Nuprl Definition : bm_firsti
bm_firsti(m) ==
binary_map_ind(m;inr ⋅ ;key,value,cnt,left,right,rec1,rec2.if bm_isEmpty(left) then inl <key, value> else rec1 fi )
Definitions occuring in Statement :
bm_isEmpty: bm_isEmpty(m),
binary_map_ind: binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]),
ifthenelse: if b then t else f fi ,
it: ⋅,
pair: <a, b>,
inr: inr x ,
inl: inl x
FDL editor aliases :
bm_firsti
bm\_firsti(m) ==
binary\_map\_ind(m;inr \mcdot{} ;key,value,cnt,left,right,rec1,rec2.if bm\_isEmpty(left)
then inl <key, value>
else rec1
fi )
Date html generated:
2015_07_17-AM-08_18_51
Last ObjectModification:
2012_08_20-PM-07_01_55
Home
Index