Nuprl Definition : pi-subst
pi-subst(t;x;p) == pi-subst-aux(p) [t / pi-names(p)] [<x, t>]
Definitions occuring in Statement :
pi-subst-aux: pi-subst-aux(p),
pi-names: pi-names(p),
cons: [a / b],
nil: [],
apply: f a,
pair: <a, b>
FDL editor aliases :
pi-subst
Latex:
pi-subst(t;x;p) == pi-subst-aux(p) [t / pi-names(p)] [<x, t>]
Date html generated:
2015_07_23-AM-11_33_45
Last ObjectModification:
2012_08_30-PM-01_19_24
Home
Index