size of an object

Stream: Is there code for X?

[Alexandre Rademaker]

Is there a way to inspect the size of an object? Say I defined

def test := [1,2,3]

What is the “sizeof” test?

[Markus Himmel]

Are you referring to the size as defined via docs#SizeOf ? If so, you can do

#reduce sizeOf test

which will tell you that it is 10.

[Alexandre Rademaker]

Not really. I am talking about memory usage

[Alexandre Rademaker]

In this case. A linked list with 3 Int elements would be something like 3*(4 + 8) assuming 4 bytes to each Int and 8 bytes for a pointer to the next item.

[Markus Himmel]

In that case you could refer to https://github.com/leanprover/lean4/blob/master/doc/dev/ffi.md#translating-types-from-lean-to-c for the details. In your case, each item of the linked list consists of an 8-byte object header, an 8-byte natural number and an 8-byte pointer to the next item. The nil at the end of the list does not take any additional space as its constructor index is stored in place of the pointer. So the memory usage should be 3*(8 + 8 + 8) bytes in total.