Nuprl Definition : apply-alist

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


Definitions occuring in Statement :  list_ind: list_ind,  ifthenelse: if b then t else f fi ,  it: ⋅,  pi1: fst(t),  pi2: snd(t),  apply: f a,  inr: inr x ,  inl: inl x
Definitions occuring in definition :  list_ind: list_ind,  inr: inr x ,  it: ⋅,  ifthenelse: if b then t else f fi ,  apply: f a,  pi1: fst(t),  inl: inl x,  pi2: snd(t)
FDL editor aliases :  apply-alist
Latex:
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