Nuprl Definition : ratsign
ratsign(x) == eval a = fst(x) in if a <z 0 then -1 if 0 <z a then 1 else 0 fi
Definitions occuring in Statement :
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
pi1: fst(t),
minus: -n,
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
pi1: fst(t),
minus: -n,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
natural_number: $n
FDL editor aliases :
ratsign
Latex:
ratsign(x) == eval a = fst(x) in if a <z 0 then -1 if 0 <z a then 1 else 0 fi
Date html generated:
2019_10_30-AM-09_34_56
Last ObjectModification:
2019_01_17-AM-10_22_09
Theory : reals
Home
Index