Fixed width integers

Stream: new members

[padawan]

Hi guys, total noob here.

I am starting to look at Lean a little. For a long time I have been a supporter of more powerful type systems in programming languages, and Lean seems to go in that direction.
That implies that I am interested in using Lean as a programming language. And there is something about this that I find a little odd: I saw unsigned 8, 16, 32, 64 bit integers, but not signed integers.
If I understand correctly, the Int type can have virtually unlimited values.

Is that correct? Is there a workaround to have more CPUI friendly values?

Thanks a lot

[David Renshaw]

There's an open issue about that: lean4#3162

[padawan]

Thank you. So from that link it looks like I could implement my own signed types.
Is that correct? Can I do the same for, say, floats?

Also, how does it work with C interoperability?

[Filippo A. E. Nuccio]

(deleted)