Nuprl Definition : bm_mapi
bm_mapi(f;m) == binary_map_ind(m;bm_E();key,value,cnt,left,right,recL,recR.bm_T(key;f key value;cnt;recL;recR))
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]),
bm_T: bm_T(key;value;cnt;left;right),
bm_E: bm_E(),
apply: f a
FDL editor aliases :
bm_mapi
Latex:
bm\_mapi(f;m) ==
binary\_map\_ind(m;bm\_E();key,value,cnt,left,right,recL,recR.bm\_T(key;f key value;cnt;recL;recR))
Date html generated:
2016_05_17-PM-01_43_12
Last ObjectModification:
2012_08_30-AM-10_03_18
Theory : binary-map
Home
Index