Nuprl Definition : apply_alist

This version of apply alist assumes that the thing ⌜x⌝ being looked for
occurs in the association list.

Another version ⌜apply-alist(eq;L;x)⌝ will return ⌜inr ⋅ ⌝ when x does
not occur.⋅
apply_alist(eq;L;x) ==  let a,more = L in let x',v = a in case eq x' x of inl(_) => v | inr(_) => apply_alist(eq;more;x)


Definitions occuring in Statement :  apply: f a,  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply: f a
FDL editor aliases :  apply_alist
Latex:
apply\_alist(eq;L;x)  ==
    let  a,more  =  L 
    in  let  x',v  =  a 
          in  case  eq  x'  x  of  inl($_{}$)  =>  v  |  inr($_{}$)  =>  appl\000Cy\_alist(eq;more;x)


Date html generated: 2019_06_20-PM-00_42_38
Last ObjectModification: 2019_02_28-PM-00_01_35

Theory : list_0


Home Index