Maximum Int in Idris

Question

How do I get maxBound of Int in Idris? I want to write my code such that it works both when the word size is 32-bit and 64-bit, and I think that will change the size of the Int.

Answer 1

I don't believe there is such a function in Idris. I think I asked this question on the language forum a while back, and the answer was no, but I might be misremembering.

That said, you seem to be assuming that Int and int have the same width for every platform. I don't know if that's true, but if it were, you could write an FFI function to get INT_MAX from #include <limits.h>.

Really though, I'd ask if you need to use a C int (and Idris Int) at all, and whether you can use int32_t and Int32, or int64_t and Int64.