Nuprl Definition : mk_lambdas-fun
mk_lambdas-fun(F;G;n;m) ==
fix((λmk_lambdas-fun,G,n. if m ≤z n then F G else λx.(mk_lambdas-fun (λf.(G f x)) (n + 1)) fi )) G n
Definitions occuring in Statement :
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
lambda: λx.A[x],
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
mk_lambdas-fun
Latex:
mk\_lambdas-fun(F;G;n;m) ==
fix((\mlambda{}mk$_{lambdas-fun}$,G,n. if m \mleq{}z n then F G else \mlambda{}x.(mk$_{lam\000Cbdas-fun}$ (\mlambda{}f.(G f x)) (n + 1)) fi )) G n
Date html generated:
2016_05_15-PM-02_09_41
Last ObjectModification:
2015_09_23-AM-07_38_08
Theory : untyped!computation
Home
Index