Nuprl Definition : bm_first
bm_first(m) ==
binary_map_ind(m;inr ⋅ ;key,value,cnt,left,right,rec1,rec2.if bm_isEmpty(left) then inl 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: ⋅,
inr: inr x ,
inl: inl x
FDL editor aliases :
bm_first
Latex:
bm\_first(m) ==
binary\_map\_ind(m;inr \mcdot{} ;key,value,cnt,left,right,rec1,rec2.if bm\_isEmpty(left)
then inl value
else rec1
fi )
Date html generated:
2016_05_17-PM-01_39_24
Last ObjectModification:
2012_08_20-PM-07_03_03
Theory : binary-map
Home
Index