Nuprl Definition : binary_map_case
binary_map_case(m;E;key,value,cnt,left,right.F[key; value; cnt; left; right]) ==
binary_map_ind(m;E;key,value,cnt,left,right,_,__.F[key; value; cnt; left; right])
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])
FDL editor aliases :
binary_map_case
Latex:
binary\_map\_case(m;E;key,value,cnt,left,right.F[key; value; cnt; left; right]) ==
binary\_map\_ind(m;E;key,value,cnt,left,right,$_{}$,\_$_{}$.F\000C[key; value; cnt; left; right])
Date html generated:
2016_05_17-PM-01_37_50
Last ObjectModification:
2014_04_30-PM-03_52_43
Theory : binary-map
Home
Index