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 of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x subtract: 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: 2016_05_17-PM-01_47_56
Last ObjectModification: 2013_04_15-PM-02_49_39

Theory : datatype-signatures

Home Index