diff options
Diffstat (limited to 'proofs/signatures/th_real.plf')
| -rw-r--r-- | proofs/signatures/th_real.plf | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf new file mode 100644 index 000000000..3478e23ef --- /dev/null +++ b/proofs/signatures/th_real.plf @@ -0,0 +1,25 @@ +(declare Real sort) + +(define arithpred_Real (! x (term Real) + (! y (term Real) + formula))) + +(declare >_Real arithpred_Real) +(declare >=_Real arithpred_Real) +(declare <_Real arithpred_Real) +(declare <=_Real arithpred_Real) + +(define arithterm_Real (! x (term Real) + (! y (term Real) + (term Real)))) + +(declare +_Real arithterm_Real) +(declare -_Real arithterm_Real) +(declare *_Real arithterm_Real) ; is * ok to use? +(declare /_Real arithterm_Real) ; is / ok to use? + +; a constant term +(declare a_real (! x mpq (term Real))) + +; unary negation +(declare u-_Real (! t (term Real) (term Real))) |