Does lean 4 support unboxing?

Stream: new members

[Diego Antonio Rosario Palomino]

hello, i am an idris/ haskell programming eyeing lean4 as another language to learn. One thing that would contribute towards deciding to learn this language would be if lean4 supported unboxed data structures.

There are a couple ways to do this. Mlton accomplishes this by monorphizing every piece of code.

On the other hand there is this : https://github.com/ollef/sixten/issues/149#issuecomment-2728964852

[Henrik Böving]

Some values like the various UInt types, enum inductives and single field structures are already represented as their native C counterpart or just the single field respectively. There is currently no unboxing for arbitrary types implemented but work on the new code generator is going to get us there eventuallym