Function lean_array_size 

pub unsafe fn lean_array_size(o: b_lean_obj_arg) -> usize

m_size of an object array (lean.h:823).

Safety

o must be a borrowed Lean array object.