diff options
Diffstat (limited to 'proofs/signatures/th_real.plf')
| -rw-r--r-- | proofs/signatures/th_real.plf | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf index 3529779f3..112328b63 100644 --- a/proofs/signatures/th_real.plf +++ b/proofs/signatures/th_real.plf @@ -4,7 +4,6 @@ (define arithpred_Real (! x (term Real) (! y (term Real) formula))) - (declare >_Real arithpred_Real) (declare >=_Real arithpred_Real) (declare <_Real arithpred_Real) @@ -29,3 +28,7 @@ ; unary negation (declare u-_Real (! t (term Real) (term Real))) + +; Is this rational positive? +(program mpq_ispos ((x mpq)) bool + (mp_ifneg x ff (mp_ifzero x ff tt))) |