Nuprl Definition : mk-lookup-list-map
mk-lookup-list-map(Key;Value;deqKey) ==
mk-map(Key;Value;lookup-list-map-type(Key;Value);lookup-list-map-eqKey(deqKey);λk,m. lookup-list-map-find(deqKey;k;m);
λk,m. lookup-list-map-inDom(deqKey;k;m);lookup-list-map-empty();λm.lookup-list-map-isEmpty(m);
λk,v,m. lookup-list-map-update(deqKey;k;v;m);λk,v,m. lookup-list-map-add(deqKey;k;v;m);
λk,m. lookup-list-map-remove(deqKey;k;m))
Definitions occuring in Statement :
lookup-list-map-remove: lookup-list-map-remove(deqKey;key;m),
lookup-list-map-add: lookup-list-map-add(deqKey;key;val;m),
lookup-list-map-update: lookup-list-map-update(deqKey;key;val;m),
lookup-list-map-isEmpty: lookup-list-map-isEmpty(m),
lookup-list-map-empty: lookup-list-map-empty(),
lookup-list-map-inDom: lookup-list-map-inDom(deqKey;key;m),
lookup-list-map-find: lookup-list-map-find(deqKey;key;m),
lookup-list-map-eqKey: lookup-list-map-eqKey(keyDeq),
lookup-list-map-type: lookup-list-map-type(Key;Value),
mk-map: mk-map(Key;Value;map;eqKey;find;inDom;empty;isEmpty;update;add;remove),
lambda: λx.A[x]
FDL editor aliases :
mk-lookup-list-map
Latex:
mk-lookup-list-map(Key;Value;deqKey) ==
mk-map(Key;Value;lookup-list-map-type(Key;Value);lookup-list-map-eqKey(deqKey);
\mlambda{}k,m. lookup-list-map-find(deqKey;k;m);\mlambda{}k,m. lookup-list-map-inDom(deqKey;k;m);
lookup-list-map-empty();\mlambda{}m.lookup-list-map-isEmpty(m);
\mlambda{}k,v,m. lookup-list-map-update(deqKey;k;v;m);\mlambda{}k,v,m. lookup-list-map-add(deqKey;k;v;m);
\mlambda{}k,m. lookup-list-map-remove(deqKey;k;m))
Date html generated:
2016_05_17-PM-01_51_43
Last ObjectModification:
2014_09_08-PM-08_37_17
Theory : datatype-signatures
Home
Index