source
def Std.Internal.UV.UDP.Socket :
Type

Represents a UDP socket.

Equations

- Std.Internal.UV.UDP.Socket = Std.Internal.UV.UDP.SocketImpl✝.type

Instances For

source
instance Std.Internal.UV.UDP.instNonemptySocket :
Nonempty Socket
source
@[extern lean_uv_udp_new]
opaque Std.Internal.UV.UDP.Socket.new :
IO Socket

Creates a new UDP socket.

source
@[extern lean_uv_udp_bind]
opaque Std.Internal.UV.UDP.Socket.bind (socket : Socket) (addr : Net.SocketAddress) :
IO Unit

Binds an UDP socket to a specific address. Address reuse is enabled to allow rebinding the same address.

source
@[extern lean_uv_udp_connect]
opaque Std.Internal.UV.UDP.Socket.connect (socket : Socket) (addr : Net.SocketAddress) :
IO Unit

Associates the UDP socket with the given address and port, so every message sent by this socket is automatically sent to that destination.

source
@[extern lean_uv_udp_send]
opaque Std.Internal.UV.UDP.Socket.send (socket : Socket) (data : Array ByteArray) (addr : Option Net.SocketAddress) :
IO (IO.Promise (Except IO.Error Unit))

Sends data through an UDP socket. The `addr` parameter specifies the destination address. If `addr` is `none`, the data is sent to the default peer address set by `connect`.

source
@[extern lean_uv_udp_recv]
opaque Std.Internal.UV.UDP.Socket.recv (socket : Socket) (size : UInt64) :
IO (IO.Promise (Except IO.Error (ByteArray × Option Net.SocketAddress)))

Receives data from an UDP socket. `size` is for the maximum bytes to receive. The promise resolves when some data is available or an error occurs. Furthermore calling this function in parallel with `waitReadable` is not supported.

source
@[extern lean_uv_udp_wait_readable]
opaque Std.Internal.UV.UDP.Socket.waitReadable (socket : Socket) :
IO (IO.Promise (Except IO.Error Unit))

Returns an `IO.Promise` that resolves once `socket` has data available for reading. Calling this function twice on the same `Socket` or in parallel with `recv` is not supported.

source
@[extern lean_uv_udp_cancel_recv]
opaque Std.Internal.UV.UDP.Socket.cancelRecv (socket : Socket) :
IO Unit

Cancels a receive operation in the form of `recv` or `waitReadable` if there is currently one pending. This resolves their returned `IO.Promise` to `none`. This function is considered dangerous, as improper use can cause data loss, and is therefore not exposed to the top-level API. Note that this function is idempotent and as such can be called multiple times on the same socket without causing errors, in particular also without a receive running in the first place.

source
@[extern lean_uv_udp_getpeername]
opaque Std.Internal.UV.UDP.Socket.getPeerName (socket : Socket) :
IO Net.SocketAddress

Receives data from an UDP socket. `size` is for the maximum bytes to receive. The promise resolves when some data is available or an error occurs. If the socket has not been previously bound with `bind`, it is automatically bound to `0.0.0.0` (all interfaces) with a random port.

source
@[extern lean_uv_udp_getsockname]
opaque Std.Internal.UV.UDP.Socket.getSockName (socket : Socket) :
IO Net.SocketAddress

Gets the local address of a bound UDP socket.

source
@[extern lean_uv_udp_set_broadcast]
opaque Std.Internal.UV.UDP.Socket.setBroadcast (socket : Socket) (on : Bool) :
IO Unit

Enables or disables broadcasting on a UDP socket.

source
@[extern lean_uv_udp_set_multicast_loop]
opaque Std.Internal.UV.UDP.Socket.setMulticastLoop (socket : Socket) (on : Bool) :
IO Unit

Enables or disables multicast loopback for a UDP socket.

source
@[extern lean_uv_udp_set_multicast_ttl]
opaque Std.Internal.UV.UDP.Socket.setMulticastTTL (socket : Socket) (ttl : UInt32) :
IO Unit

Sets the time-to-live (TTL) value for multicast packets.

source
@[extern lean_uv_udp_set_membership]
opaque Std.Internal.UV.UDP.Socket.setMembership (socket : Socket) (multicastAddr : Net.IPAddr) (interfaceAddr : Option Net.IPAddr) (membership : UInt8) :
IO Unit

Sets the membership for joining or leaving a multicast group. If `interfaceAddr` is `none`, the default network interface is used.

source
@[extern lean_uv_udp_set_multicast_interface]
opaque Std.Internal.UV.UDP.Socket.setMulticastInterface (socket : Socket) (interfaceAddr : Net.IPAddr) :
IO Unit

Sets the multicast interface for sending packets.

source
@[extern lean_uv_udp_set_ttl]
opaque Std.Internal.UV.UDP.Socket.setTTL (socket : Socket) (ttl : UInt32) :
IO Unit

Sets the TTL value for outgoing packets.