Function lean_sys::lean_object_byte_size

pub unsafe extern "C" fn lean_object_byte_size(
    o: *mut lean_object
) -> usize

The object size may be slightly bigger for constructor objects. The runtime does not track the size of the scalar size area. All constructor objects are “small”, and allocated into pages. We retrieve their size by accessing the page header. The size of small objects is a multiple of LEAN_OBJECT_SIZE_DELTA