Available arithmetic types provided in prelude

[Yannick Duchêne]

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 `dataprop`s 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 `dataprop`s/axioms/proofs matching my need for bounded non‑modulus arithmetic (better to ask before).

[gmhwxi]

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.dats