Zulip Chat Archive
Stream: new members
Topic: Fixed width integers
padawan (Mar 03 2024 at 21:24):
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 (Mar 03 2024 at 21:30):
There's an open issue about that: lean4#3162
padawan (Mar 03 2024 at 21:46):
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 (Mar 11 2024 at 12:38):
(deleted)
Last updated: May 02 2025 at 03:31 UTC