Nuprl Definition : bool-size
𝔹size(k;f) == primrec(k;0;λn,m. (if f n then 1 else 0 fi + m))
Definitions occuring in Statement :
primrec: primrec(n;b;c),
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
primrec: primrec(n;b;c),
lambda: λx.A[x],
add: n + m,
ifthenelse: if b then t else f fi ,
apply: f a,
natural_number: $n
FDL editor aliases :
bool-size
Latex:
\mBbbB{}size(k;f) == primrec(k;0;\mlambda{}n,m. (if f n then 1 else 0 fi + m))
Date html generated:
2016_05_15-PM-04_43_28
Last ObjectModification:
2015_09_23-AM-07_49_50
Theory : general
Home
Index