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