Function lean_int64_of_int

lean_py/_runtime.py:668–676

(self, p)

        return big(n)

    def lean_int64_of_int(self, p):
        fn = self._find_leanpy_helper("leanpy_int64_of_int")
        if fn is not None:
            fn.argtypes = [LeanObjectPtr]
            fn.restype = c_int64
            return int(fn(p))
        if self.lean_is_scalar(p):
            return int(self.lean_scalar_to_int(p))
        raise RuntimeError("leanpy_int64_of_int not found")

    def lean_scalar_to_int(self, p):
        # The C runtime encodes Int as `lean_box((unsigned)(int)n)`, so