diff options
Diffstat (limited to 'src/lfsc/tests/signatures/th_int.plf')
| -rw-r--r-- | src/lfsc/tests/signatures/th_int.plf | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/lfsc/tests/signatures/th_int.plf b/src/lfsc/tests/signatures/th_int.plf new file mode 100644 index 0000000..9a0a2d6 --- /dev/null +++ b/src/lfsc/tests/signatures/th_int.plf @@ -0,0 +1,25 @@ +(declare Int sort) + +(define arithpred_Int (! x (term Int) + (! y (term Int) + formula))) + +(declare >_Int arithpred_Int) +(declare >=_Int arithpred_Int) +(declare <_Int arithpred_Int) +(declare <=_Int arithpred_Int) + +(define arithterm_Int (! x (term Int) + (! y (term Int) + (term Int)))) + +(declare +_Int arithterm_Int) +(declare -_Int arithterm_Int) +(declare *_Int arithterm_Int) ; is * ok to use? +(declare /_Int arithterm_Int) ; is / ok to use? + +; a constant term +(declare a_int (! x mpz (term Int))) + +; unary negation +(declare u-_Int (! t (term Int) (term Int))) |