Nuprl Definition : bm_listItemsi_d2l
bm_listItemsi_d2l(m) == binary_map_ind(m;λl.l;key,value,cnt,left,right,recL,recR.λl.(recL [<key, value> / (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],
pair: <a, b>
FDL editor aliases :
bm_listItemsi_d2l
Latex:
bm\_listItemsi\_d2l(m) ==
binary\_map\_ind(m;\mlambda{}l.l;key,value,cnt,left,right,recL,recR.\mlambda{}l.(recL [<key, value> / (recR l)]))
Date html generated:
2016_05_17-PM-01_42_35
Last ObjectModification:
2012_08_28-PM-01_01_51
Theory : binary-map
Home
Index