Nuprl Definition : binary_map
binary_map(T;Key) ==  {p:binary_mapco(T;Key)| (binary_mapco_size(p))↓} 
Definitions occuring in Statement : 
binary_mapco_size: binary_mapco_size(p)
, 
binary_mapco: binary_mapco(T;Key)
, 
has-value: (a)↓
, 
set: {x:A| B[x]} 
FDL editor aliases : 
binary_map
Latex:
binary\_map(T;Key)  ==    \{p:binary\_mapco(T;Key)|  (binary\_mapco\_size(p))\mdownarrow{}\} 
Date html generated:
2016_05_17-PM-01_36_59
Last ObjectModification:
2014_04_30-AM-11_05_20
Theory : binary-map
Home
Index