Socket.Socket

source

@[extern lean_socket_mk]

constant Socket.Socket.mk (d : Socket.AddressFamily) (t : Socket.SockType) :

IO Socket.Socket

Create a new Socket using the specified domain and type.

source

@[extern lean_socket_close]

constant Socket.Socket.close (s : Socket.Socket) :

IO Unit

Close the Socket.

NOTE: Although Socket is designed to be automatically closed when garbage collected, it's a good practice to manually close it beforehand.

source

@[extern lean_socket_connect]

constant Socket.Socket.connect (s : Socket.Socket) (a : Socket.SockAddr) :

IO Unit

Initiate a connection on a socket.

source

@[extern lean_socket_bind]

constant Socket.Socket.bind (s : Socket.Socket) (a : Socket.SockAddr) :

IO Unit

Bind a name to a socket.

source

@[extern lean_socket_listen]

constant Socket.Socket.listen (s : Socket.Socket) (n : UInt8) :

IO Unit

Listen for connections on a socket.

source

@[extern lean_socket_accept]

constant Socket.Socket.accept (s : Socket.Socket) :

IO (Socket.SockAddr × Socket.Socket)

Accept a connection on a socket.

source

@[extern lean_socket_send]

constant Socket.Socket.send (s : Socket.Socket) (b : ByteArray) :

IO USize

Send a message from a socket.

source

@[extern lean_socket_recv]

constant Socket.Socket.recv (s : Socket.Socket) (n : USize) :

IO ByteArray

Receive a message from a socket.

source

@[extern lean_socket_sendto]

constant Socket.Socket.sendto (s : Socket.Socket) (b : ByteArray) (a : Socket.SockAddr) :

IO USize

Send a message from a socket.

source

@[extern lean_socket_recvfrom]

constant Socket.Socket.recvfrom (s : Socket.Socket) (n : USize) :

IO (Socket.SockAddr × ByteArray)

Receive a message from a socket.

source

@[extern lean_socket_shutdown]

constant Socket.Socket.shutdown (s : Socket.Socket) (h : Socket.ShutdownHow) :

IO Unit

Shut down part of a full-duplex connection.

source

@[extern lean_socket_peer]

constant Socket.Socket.peer (s : Socket.Socket) :

IO Socket.SockAddr

Get address of connected peer.