Nuprl Definition : apply-alist

apply-alist(eq;L;x) ==  rec-case(L) of [] => inr ⋅  p::ps => r.if eq (fst(p)) then inl (snd(p)) else fi 

Definitions occuring in Statement :  list_ind: list_ind ifthenelse: if then else fi  it: pi1: fst(t) pi2: snd(t) apply: a inr: inr  inl: inl x
Definitions occuring in definition :  list_ind: list_ind inr: inr  it: ifthenelse: if then else fi  apply: a pi1: fst(t) inl: inl x pi2: snd(t)
FDL editor aliases :  apply-alist

apply-alist(eq;L;x)  ==
    rec-case(L)  of
    []  =>  inr  \mcdot{} 
    p::ps  =>
      r.if  eq  (fst(p))  x  then  inl  (snd(p))  else  r  fi 

Date html generated: 2016_05_14-AM-06_46_55
Last ObjectModification: 2015_12_03-PM-02_07_35

Theory : list_0

Home Index