Nuprl Definition : pi-simple-subst
pi-simple-subst(t;x;P) == pi-simple-subst-aux(t;x;P;[t / pi-names(P)])
Definitions occuring in Statement :
pi-simple-subst-aux: pi-simple-subst-aux(t;x;P;avoid),
pi-names: pi-names(p),
cons: [a / b]
FDL editor aliases :
pi-simple-subst
Latex:
pi-simple-subst(t;x;P) == pi-simple-subst-aux(t;x;P;[t / pi-names(P)])
Date html generated:
2015_07_23-AM-11_33_47
Last ObjectModification:
2012_08_30-PM-01_19_29
Home
Index