Function lean_array_set_core 

pub unsafe fn lean_array_set_core(
    o: *mut lean_object,
    i: usize,
    v: lean_obj_arg,
)

Write element i of an object array (lean.h:842–848).

Safety

o must be a unique (exclusive) Lean array object and i < lean_array_size(o). The caller transfers ownership of v.