Nuprl Definition : reg-seq-list-add
reg-seq-list-add(L) == λn.cbv_list_accum(s,a.s + (a n);0;L)
Definitions occuring in Statement :
cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),
add: n + m,
apply: f a,
natural_number: $n
FDL editor aliases :
reg-seq-list-add
Latex:
reg-seq-list-add(L) == \mlambda{}n.cbv\_list\_accum(s,a.s + (a n);0;L)
Date html generated:
2016_05_18-AM-06_48_06
Last ObjectModification:
2015_09_23-AM-09_00_38
Theory : reals
Home
Index