Nuprl Definition : enumerate
enumerate(P;n) == primrec(n;mu(P);λi,r. eval r' = r + 1 in r' + mu(λk.(P (r' + k))))
Definitions occuring in Statement :
mu: mu(f),
primrec: primrec(n;b;c),
callbyvalue: callbyvalue,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
primrec: primrec(n;b;c),
callbyvalue: callbyvalue,
natural_number: $n,
mu: mu(f),
lambda: λx.A[x],
apply: f a,
add: n + m
FDL editor aliases :
enumerate
Latex:
enumerate(P;n) == primrec(n;mu(P);\mlambda{}i,r. eval r' = r + 1 in r' + mu(\mlambda{}k.(P (r' + k))))
Date html generated:
2016_05_15-PM-05_27_25
Last ObjectModification:
2015_09_23-AM-07_54_23
Theory : general
Home
Index