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