Nuprl Definition : int-decr-map-add
int-decr-map-add(k;v;m) == insert-combine(int-minus-comparison(λp.(fst(p)));λx,a. a;<k, v>;m)
Definitions occuring in Statement :
insert-combine: insert-combine(cmp;f;x;l),
int-minus-comparison: int-minus-comparison(f),
pi1: fst(t),
lambda: λx.A[x],
pair: <a, b>
FDL editor aliases :
int-decr-map-add
int-decr-map-add(k;v;m) == insert-combine(int-minus-comparison(\mlambda{}p.(fst(p)));\mlambda{}x,a. a;<k, v>m)
Date html generated:
2015_07_17-AM-08_23_25
Last ObjectModification:
2013_04_17-PM-03_40_17
Home
Index