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: f 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