Nuprl Definition : int2nat
int2nat(i) == eval j = i in if (j) < (0) then (2 * ((-j) - 1)) + 1 else (2 * j)
Definitions occuring in Statement :
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
multiply: n * m,
subtract: n - m,
add: n + m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
add: n + m,
subtract: n - m,
minus: -n,
multiply: n * m,
natural_number: $n
FDL editor aliases :
int2nat
Latex:
int2nat(i) == eval j = i in if (j) < (0) then (2 * ((-j) - 1)) + 1 else (2 * j)
Date html generated:
2019_06_20-PM-02_52_03
Last ObjectModification:
2019_02_07-PM-06_31_32
Theory : continuity
Home
Index