Nuprl Definition : int-to-real
r(n) == λk.(2 * k * n)
Definitions occuring in Statement :
lambda: λx.A[x],
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
natural_number: $n,
multiply: n * m
FDL editor aliases :
i2r
Latex:
r(n) == \mlambda{}k.(2 * k * n)
Date html generated:
2016_05_18-AM-06_47_55
Last ObjectModification:
2015_09_23-AM-09_00_38
Theory : reals
Home
Index