Module array 

Object and scalar arrays — externs and inline accessors from lean.h:815–1028.

Functions

lean_alloc_array^⚠

Allocate a freshly initialised object array (lean.h:816–822).

lean_alloc_sarray^⚠

Allocate a freshly initialised scalar-array (lean.h:1004–1010).

lean_array_capacity^⚠

m_capacity of an object array (lean.h:824).

lean_array_cptr^⚠

Pointer to the array’s element storage (lean.h:831).

lean_array_get_core^⚠

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

lean_array_get_panic^⚠

lean_array_mk^⚠

lean_array_push^⚠

lean_array_set_core^⚠

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

lean_array_set_panic^⚠

lean_array_size^⚠

m_size of an object array (lean.h:823).

lean_array_to_list^⚠

lean_mk_array^⚠

lean_sarray_capacity^⚠

m_capacity of a scalar array (lean.h:1015).

lean_sarray_cptr^⚠

Pointer to the scalar array’s byte storage (lean.h:1028).

lean_sarray_elem_size^⚠

Element size of a scalar array (lean.h:1011–1014).

lean_sarray_size^⚠

m_size of a scalar array (lean.h:1019).