Skip to main content

lean_array_get_core

Function lean_array_get_core 

Source
pub unsafe fn lean_array_get_core(
    o: b_lean_obj_arg,
    i: usize,
) -> *mut lean_object
Expand description

Borrow element i of an object array (lean.h:838–841).

§Safety

o must be a borrowed Lean array object and i < lean_array_size(o).