Function lean_array_set_core

src/array/low_level.rs:56–62

(o: u_lean_obj_arg, i: usize, v: lean_obj_arg)

#[inline(always)]
pub unsafe fn lean_array_set_core(o: u_lean_obj_arg, i: usize, v: lean_obj_arg) {
    debug_assert!(!lean_has_rc(o) || lean_is_exclusive(o));
    debug_assert!(i < lean_array_size(o));
    (raw_field!(lean_to_array(o), lean_array_object, m_data) as *mut *mut lean_object)
        .add(i)
        .write(v)
}

extern "C" {
    pub fn lean_array_mk(l: lean_obj_arg) -> *mut lean_object;