Function lean_sarray_size 

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

m_size of a scalar array (lean.h:1019).

Safety

o must be a borrowed Lean scalar-array object.