Function lean_alloc_array 

pub unsafe fn lean_alloc_array(size: usize, capacity: usize) -> lean_obj_res

Allocate a freshly initialised object array (lean.h:816–822).

Returns a LeanArray-tagged object with m_size = size, m_capacity = capacity, and capacity uninitialised *mut lean_object slots. The caller installs each slot via lean_array_set_core before the array escapes; the first size slots become the visible elements.

Safety

• size <= capacity.
• size_of::<LeanArrayObjectRepr>() + size_of::<*mut lean_object>() * capacity must not overflow usize; the helper checks this with strict_* arithmetic and panics on overflow.
• Every one of the first size element slots must be initialised with a live owned *mut lean_object (matching the C convention that lean_dec on the array recursively decrements each visible element) before the array is observed by any other Lean code.