Nuprl Definition : int-decr-map-find
int-decr-map-find(k;m) == case find-combine(λp.(k - fst(p));m) of inl(x) => inl (snd(x)) | inr(x) => inr ⋅
Definitions occuring in Statement :
find-combine: find-combine(cmp;l),
it: ⋅,
pi1: fst(t),
pi2: snd(t),
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
subtract: n - m
FDL editor aliases :
int-decr-map-find
int-decr-map-find(k;m) ==
case find-combine(\mlambda{}p.(k - fst(p));m) of inl(x) => inl (snd(x)) | inr(x) => inr \mcdot{}
Date html generated:
2015_07_17-AM-08_22_45
Last ObjectModification:
2013_04_15-PM-02_49_39
Home
Index