Nuprl Definition : name-subst

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


Definitions occuring in Statement :  name-deq: NameDeq,  apply-alist: apply-alist(eq;L;x),  decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :  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
Latex:
name-subst(s;x)  ==    case  apply-alist(NameDeq;s;x)  of  inl(z)  =>  z  |  inr(z)  =>  x


Date html generated: 2016_05_14-PM-03_35_05
Last ObjectModification: 2015_09_22-PM-06_01_06

Theory : decidable!equality


Home Index