Nuprl Definition : bm_collate_left
bm_collate_left(m) ==
binary_map_ind(m;λrest.rest;key,value,cnt,left,right,recL,recR.λrest.(recL [bm_T(key;value;cnt;left;right) / rest]))
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),
cons: [a / b],
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
bm_collate_left
Latex:
bm\_collate\_left(m) ==
binary\_map\_ind(m;\mlambda{}rest.rest;key,value,cnt,left,right,recL,recR.\mlambda{}rest.(recL
[... /
rest]))
Date html generated:
2016_05_17-PM-01_42_59
Last ObjectModification:
2012_08_28-PM-01_43_56
Theory : binary-map
Home
Index