Nuprl Definition : bm_listKeys_d2l

bm_listKeys_d2l(m) ==  binary_map_ind(m;λl.l;key,value,cnt,left,right,recL,recR.λl.(recL [key (recR l)]))



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]) cons: [a b] apply: a lambda: λx.A[x]
FDL editor aliases :  bm_listKeys_d2l
bm\_listKeys\_d2l(m)  ==
    binary\_map\_ind(m;\mlambda{}l.l;key,value,cnt,left,right,recL,recR.\mlambda{}l.(recL  [key  /  (recR  l)]))



Date html generated: 2015_07_17-AM-08_20_19
Last ObjectModification: 2012_08_28-PM-01_06_13

Home Index