Documentation

Socket.SockAddr

@[extern lean_sockaddr_mk]

constant Socket.SockAddr.mk (host : String) (port : String) (family : optParam Socket.AddressFamily Socket.AddressFamily.unspecified) (type : optParam Socket.SockType Socket.SockType.unspecified) :

IO Socket.SockAddr

Create a SockAddr.

@[extern lean_sockaddr_family]

constant Socket.SockAddr.family (a : Socket.SockAddr) :

Option Socket.AddressFamily

Get family of the SockAddr.

@[extern lean_sockaddr_port]

constant Socket.SockAddr.port (a : Socket.SockAddr) :

Get family of the SockAddr.

@[extern lean_sockaddr_host]

constant Socket.SockAddr.host (a : Socket.SockAddr) :

Get family of the SockAddr.

instance Socket.instToStringSockAddr :

ToString Socket.SockAddr

Equations

Socket.instToStringSockAddr = { toString := fun a => let host := Option.getD (Socket.SockAddr.host a) "none"; let port := Option.getD (Option.map (fun a => toString "" ++ toString a ++ toString "") (Socket.SockAddr.port a)) "none"; let family := Option.getD (Option.map (fun a => toString "" ++ toString a ++ toString "") (Socket.SockAddr.family a)) "none"; toString "(" ++ toString host ++ toString ", " ++ toString port ++ toString ", " ++ toString family ++ toString ")" }

Convert SockAddr to String.