Available arithmetic types provided in prelude

Google Group
1

Looking at the dataprop and axioms and proofs in arith_prf.sats (note:
I’m talking about ATS2, I don’t use ATS1), for multiplication,
division/modulus and exponentiation, I noticed there is no range condition,
and the dataprops and proofs are valid for modulus arithmetic only
(unless I’ve missed or misunderstood something).

That’s not to beg for anything, this just to know: is this all the of
arithmetic provided with ATS2 or is there also bounded arithmetic somewhere?

I’m just wondering before devising to create some dataprops/axioms/proofs
matching my need for bounded non‑modulus arithmetic (better to ask before).

2

So far, there is no significant work in ATS on handling integer arithmetic
overflow.

Here is a relevant example I did a while ago:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/arith_overflow.datsOn Thursday, August 7, 2014 9:17:48 PM UTC-4, Yannick Duchêne wrote:

Looking at the dataprop and axioms and proofs in arith_prf.sats (note:
I’m talking about ATS2, I don’t use ATS1), for multiplication,
division/modulus and exponentiation, I noticed there is no range condition,
and the dataprops and proofs are valid for modulus arithmetic only
(unless I’ve missed or misunderstood something).

That’s not to beg for anything, this just to know: is this all the of
arithmetic provided with ATS2 or is there also bounded arithmetic somewhere?

I’m just wondering before devising to create some
dataprops/axioms/proofs matching my need for bounded non‑modulus
arithmetic (better to ask before).