Function lean_array_get_core

lean_py/_runtime.py:530–536

(self, o, i)

        return arr.contents.m_size

    def lean_array_get_core(self, o, i):
        arr_cls = structs.get("lean_array_object")
        arr = ctypes.cast(o, POINTER(arr_cls))
        offset = arr_cls.m_data.offset
        addr = ctypes.addressof(arr.contents) + offset
        ptr_array = ctypes.cast(addr, POINTER(LeanObjectPtr * (i + 1)))
        return ptr_array.contents[i]

    def lean_string_size(self, o):
        str_cls = structs.get("lean_string_object")