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
Latex:
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:
2016_05_17-PM-01_39_28
Last ObjectModification:
2012_08_20-PM-07_01_55
Theory : binary-map
Home
Index