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