Nuprl Definition : qabs
|r| == let r' ⟵ r in if qpositive(r') then r' else -(r') fi
Definitions occuring in Statement :
qpositive: qpositive(r),
qmul: r * s,
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
minus: -n,
natural_number: $n
Definitions occuring in definition :
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
qpositive: qpositive(r),
qmul: r * s,
minus: -n,
natural_number: $n
FDL editor aliases :
qabs
Latex:
|r| == let r' \mleftarrow{}{} r in if qpositive(r') then r' else -(r') fi
Date html generated:
2016_05_15-PM-10_44_35
Last ObjectModification:
2015_09_23-AM-08_27_17
Theory : rationals
Home
Index