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

Function lean_string_size

lean_py/_runtime.py:538–541  ·  view source on GitHub ↗
(self, o)

Source from the content-addressed store, hash-verified

536 return ptr_array.contents[i]
537
538 def lean_string_size(self, o):
539 str_cls = structs.get("lean_string_object")
540 s = ctypes.cast(o, POINTER(str_cls))
541 return s.contents.m_size
542
543 def lean_string_len(self, o):
544 str_cls = structs.get("lean_string_object")

Callers 1

lean_py_of_stringFunction · 0.85

Calls 1

getMethod · 0.45

Tested by

no test coverage detected