MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / lean_array_set_core

Function lean_array_set_core

lean_py/_runtime.py:572–578  ·  view source on GitHub ↗
(self, o, i, v)

Source from the content-addressed store, hash-verified

570 return fn(size, capacity)
571
572 def lean_array_set_core(self, o, i, v):
573 arr_cls = structs.get("lean_array_object")
574 arr = ctypes.cast(o, POINTER(arr_cls))
575 offset = arr_cls.m_data.offset
576 addr = ctypes.addressof(arr.contents) + offset
577 ptr_array = ctypes.cast(addr, POINTER(LeanObjectPtr * (i + 1)))
578 ptr_array.contents[i] = v
579
580 # ----- Numeric conversions (inline in lean.h) -----
581 def lean_box_uint64(self, v):

Callers 2

leanpy_array_set_coreFunction · 0.85
leancallable_callFunction · 0.85

Calls 1

getMethod · 0.45

Tested by

no test coverage detected