Nuprl Definition : sign
sign(x) == if 0 ≤z x then 1 else -1 fi
Definitions occuring in Statement :
le_int: i ≤z j,
ifthenelse: if b then t else f fi ,
minus: -n,
natural_number: $n
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
minus: -n,
natural_number: $n
FDL editor aliases :
sign
Latex:
sign(x) == if 0 \mleq{}z x then 1 else -1 fi
Date html generated:
2016_05_14-PM-04_28_07
Last ObjectModification:
2015_09_22-PM-06_02_59
Theory : num_thy_1
Home
Index