Nuprl Definition : evodd-succ
evodd-succ(n) == pW-sup(inr Ax ;λx.n)
Definitions occuring in Statement :
pW-sup: pW-sup(a;f)
,
lambda: λx.A[x]
,
inr: inr x
,
axiom: Ax
Definitions occuring in definition :
pW-sup: pW-sup(a;f)
,
inr: inr x
,
axiom: Ax
,
lambda: λx.A[x]
FDL editor aliases :
evodd-succ
Latex:
evodd-succ(n) == pW-sup(inr Ax ;\mlambda{}x.n)
Date html generated:
2016_05_14-AM-06_14_41
Last ObjectModification:
2015_09_22-PM-05_47_14
Theory : co-recursion
Home
Index