Function lean_box_float

lean_py/_runtime.py:600–610

(self, v)

        return self.lean_unbox(o)

    def lean_box_float(self, v):
        # `lean_box_float` is `static inline` in lean.h, so it's not a
        # linkable symbol — inline it: alloc a ctor with one double of
        # scalar payload and store the value at offset 0 of the
        # post-m_objs region.
        ctor = self.lean_alloc_ctor(0, 0, ctypes.sizeof(c_double))
        ctor_cls = structs.get("lean_ctor_object")
        c = ctypes.cast(ctor, POINTER(ctor_cls))
        addr = ctypes.addressof(c.contents) + ctor_cls.m_objs.offset
        ctypes.cast(addr, POINTER(c_double))[0] = v
        return ctor

    def lean_unbox_float(self, o):
        ctor_cls = structs.get("lean_ctor_object")