Nuprl Definition : partial_ap_gen
partial_ap_gen(g;n;s;m) == λf.(g mk_lambdas(mk_lambdas_fun(λh.mk_lambdas(h f;n - m - s);m);s))
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_gen
Latex:
partial\_ap\_gen(g;n;s;m) == \mlambda{}f.(g mk\_lambdas(mk\_lambdas\_fun(\mlambda{}h.mk\_lambdas(h f;n - m - s);m);s))
Date html generated:
2016_05_15-PM-02_10_07
Last ObjectModification:
2015_09_23-AM-07_38_11
Theory : untyped!computation
Home
Index