Function lean_ctor_get

lean_py/_runtime.py:467–477

(self, o, i)

        return self.lean_ptr_other(o)

    def lean_ctor_get(self, o, i):
        ctor_cls = structs.get("lean_ctor_object")
        ctor = ctypes.cast(o, POINTER(ctor_cls))
        offset = ctor_cls.m_objs.offset
        # Read the pointer value as an integer to avoid creating a ctypes
        # pointer that aliases into the Lean ctor's m_objs memory. If the
        # ctor is later freed (lean_dec), an aliased pointer would become
        # stale when the Lean allocator reuses the memory.
        elem_addr = ctypes.addressof(ctor.contents) + offset + i * ctypes.sizeof(LeanObjectPtr)
        raw_val = c_void_p.from_address(elem_addr).value or 0
        return ctypes.cast(c_void_p(raw_val), LeanObjectPtr)

    def lean_ctor_set(self, o, i, v):
        ctor_cls = structs.get("lean_ctor_object")