Nuprl Definition : simple-cbva-seq
simple-cbva-seq(L;F;m) == cbva-seq(L;if (m =z 0) then F else mk_lambdas(F;m - 1) fi ;m)
Definitions occuring in Statement :
mk_lambdas: mk_lambdas(F;m),
cbva-seq: cbva-seq(L;F;m),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
cbva-seq: cbva-seq(L;F;m),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
mk_lambdas: mk_lambdas(F;m),
subtract: n - m,
natural_number: $n
FDL editor aliases :
simple-cbva-seq
Latex:
simple-cbva-seq(L;F;m) == cbva-seq(L;if (m =\msubz{} 0) then F else mk\_lambdas(F;m - 1) fi ;m)
Date html generated:
2016_05_15-PM-02_12_11
Last ObjectModification:
2015_09_23-AM-07_38_15
Theory : untyped!computation
Home
Index