Nuprl Definition : evodd-enum
evodd-enum(n) == primrec(n;<tt, evodd-zero()>;λi,x. let b,z = x in <¬bb, evodd-succ(z)>)
Definitions occuring in Statement :
evodd-succ: evodd-succ(n),
evodd-zero: evodd-zero(),
primrec: primrec(n;b;c),
bnot: ¬bb,
btrue: tt,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
primrec: primrec(n;b;c),
btrue: tt,
evodd-zero: evodd-zero(),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
bnot: ¬bb,
evodd-succ: evodd-succ(n)
FDL editor aliases :
evodd-enum
Latex:
evodd-enum(n) == primrec(n;<tt, evodd-zero()>\mlambda{}i,x. let b,z = x in <\mneg{}\msubb{}b, evodd-succ(z)>)
Date html generated:
2016_05_14-AM-06_14_49
Last ObjectModification:
2015_09_22-PM-05_47_15
Theory : co-recursion
Home
Index