Nuprl Definition : partial_ap
partial_ap(g;n;m) == λf.(g mk_lambdas_fun(λh.mk_lambdas(h f;n - m);m))
Definitions occuring in Statement :
mk_lambdas: mk_lambdas(F;m),
mk_lambdas_fun: mk_lambdas_fun(F;m),
apply: f a,
lambda: λx.A[x],
subtract: n - m
Definitions occuring in definition :
mk_lambdas_fun: mk_lambdas_fun(F;m),
lambda: λx.A[x],
mk_lambdas: mk_lambdas(F;m),
apply: f a,
subtract: n - m
FDL editor aliases :
partial_ap
Latex:
partial\_ap(g;n;m) == \mlambda{}f.(g mk\_lambdas\_fun(\mlambda{}h.mk\_lambdas(h f;n - m);m))
Date html generated:
2016_05_15-PM-02_10_11
Last ObjectModification:
2015_09_23-AM-07_38_12
Theory : untyped!computation
Home
Index