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
Latex:
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:
2016_05_17-PM-01_49_39
Last ObjectModification:
2013_04_17-PM-03_40_17
Theory : datatype-signatures
Home
Index