(o: *const lean_object)
| 40 | |
| 41 | #[inline(always)] |
| 42 | pub unsafe fn lean_sarray_data_byte_size(o: *const lean_object) -> usize { |
| 43 | size_of::<lean_sarray_object>() + lean_sarray_elem_size(o) as usize * lean_sarray_size(o) |
| 44 | } |
| 45 | |
| 46 | #[inline(always)] |
| 47 | pub unsafe fn lean_sarray_set_size(o: u_lean_obj_arg, sz: usize) { |
nothing calls this directly
no test coverage detected