Documentation

Socket.Basic

Socket Type Definitions #

This module defines some basic types to be used across whole pacage:

Socket #

source
constant Socket.Socket.Nonempty :
NonemptyType

Use NonemptyType to implement Inhabited for Socket. detailed explanation

source
noncomputable def Socket.Socket :
Type
Equations

Opaque reference to underlying platform specific socket.

To create a Socket, refer to Socket.mk. Then you can manipulate the Socket using common socket functions like Socket.bind,Socket.connect, etc. For all functions available, refer to the Socket module.

NOTE: NonemptyType is used to implement Inhabited for Socket. detailed explanation

import Socket
open Socket

def main : IO Unit := do
  let s ← Socket.mk
  -- some socket operations
  s.close
source
noncomputable instance Socket.instNonemptySocket :
Nonempty Socket.Socket
Equations

Use NonemptyType to implement Inhabited for Socket. detailed explanation

source
constant Socket.SockAddr.Nonempty :
NonemptyType

Use NonemptyType to implement Inhabited for SockAddr. detailed explanation

source
noncomputable def Socket.SockAddr :
Type
Equations

Opaque reference to underlying socket address.

NOTE: Different from the C sockaddr, SockAddr also includes length.

source
noncomputable instance Socket.instNonemptySockAddr :
Nonempty Socket.SockAddr
Equations

Use NonemptyType to implement Inhabited for SockAddr detailed explanation

source
inductive Socket.AddressFamily :
Type

Enumeration of supported address families, which is used in Socket.mk.

source
instance Socket.instInhabitedAddressFamily :
Inhabited Socket.AddressFamily
Equations
source
instance Socket.instToStringAddressFamily :
ToString Socket.AddressFamily
Equations

Convert AddressFamily to String.

source
inductive Socket.SockType :
Type

Enumeration of supported socket types, which is used in Socket.mk.

source
instance Socket.instInhabitedSockType :
Inhabited Socket.SockType
Equations
source
instance Socket.instToStringSockType :
ToString Socket.SockType
Equations

Convert SockType to String.

source
inductive Socket.ShutdownHow :
Type

Enumeration of how is socket shutdown, which is used in Socket.shutdown.

source
instance Socket.instInhabitedShutdownHow :
Inhabited Socket.ShutdownHow
Equations
source
@[extern lean_gethostname]
constant Socket.hostname :
IO String

Get hostname of current machine.

Explanation: Usage of NonemptyType #

As Socket and SockAddr are implemented usinglean_external_class. NonemptyType is used to implement Inhabited for these types.

A simple example of this trick can be found here in Lean core.