Nuprl Definition : nat2int
nat2int(m) == if m rem 2=0 then m ÷ 2 else (-((m ÷ 2) + 1))
Definitions occuring in Statement :
int_eq: if a=b then c else d,
remainder: n rem m,
divide: n ÷ m,
add: n + m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
int_eq: if a=b then c else d,
remainder: n rem m,
minus: -n,
add: n + m,
divide: n ÷ m,
natural_number: $n
FDL editor aliases :
nat2int
Latex:
nat2int(m) == if m rem 2=0 then m \mdiv{} 2 else (-((m \mdiv{} 2) + 1))
Date html generated:
2019_06_20-PM-02_52_08
Last ObjectModification:
2019_02_06-PM-06_50_12
Theory : continuity
Home
Index