Function lean_array_pop

src/array/high_level.rs:134–145

(a: lean_obj_arg)

#[inline]
pub unsafe fn lean_array_pop(a: lean_obj_arg) -> *mut lean_object {
    let r = lean_ensure_exclusive_array(a);
    let sz = lean_array_size(a);
    if sz == 0 {
        return r;
    }
    let sz = sz - 1;
    let last = lean_array_cptr(r).add(sz);
    *(raw_field!(lean_to_array(r), lean_array_object, m_size) as *mut usize) = sz;
    lean_dec(*last);
    r
}

#[inline]
pub unsafe fn lean_array_uswap(a: lean_obj_arg, i: usize, j: usize) -> *mut lean_object {