diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/signatures/th_lira.plf | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf index 145980b24..a5b73d6b4 100644 --- a/proofs/signatures/th_lira.plf +++ b/proofs/signatures/th_lira.plf @@ -59,8 +59,14 @@ ((/_Real x y) (/_Real (reify_real_term x) (reify_real_term y))) )) -; Predicates of the form (term Integer) >= (term Real) or negations thereof -(declare >=_IntReal (! x (term Int) (! y (term Real) formula))) +; Predicates of the form (term Integer) (comparison) (term Real) +(define arithpred_IntReal (! x (term Int) + (! y (term Real) + formula))) +(declare >_IntReal arithpred_IntReal) +(declare >=_IntReal arithpred_IntReal) +(declare <_IntReal arithpred_IntReal) +(declare <=_IntReal arithpred_IntReal) ; From an arith predicate, compute the equivalent real predicate ; All arith predicates are (possibly negated) >='s with a real on the right. |