---

name-subst(s;x) ==  case apply-alist(NameDeq;s;x) of inl(z) => z | inr(z) => x

---

Definitions :  decide: case b of inl(x) => s[x] | inr(y) => t[y],  apply-alist: apply-alist(eq;L;x),  name-deq: NameDeq
FDL editor aliases :  name-subst

---

name-subst(s;x)  ==    case  apply-alist(NameDeq;s;x)  of  inl(z)  =>  z  |  inr(z)  =>  x


Date html generated: 2010_08_26-PM-11_30_03
Last ObjectModification: 2010_02_15-PM-11_18_13

Home Index