This module contains Lean representations of IP and socket addresses:

• IPv4Addr: Representing IPv4 addresses.
• SocketAddressV4: Representing a pair of IPv4 address and port.
• IPv6Addr: Representing IPv6 addresses.
• SocketAddressV6: Representing a pair of IPv6 address and port.
• IPAddr: Can either be an IPv4Addr or an IPv6Addr.
• SocketAddress: Can either be a SocketAddressV4 or SocketAddressV6.

structure Std.Net.MACAddr : Type

Representation of a MAC address.

• octets : Vector UInt8 6

  This structure represents the address: octets[0]:octets[1]:octets[2]:octets[3]:octets[4]:octets[5].

@[implicit_reducible]

instance Std.Net.instInhabitedMACAddr : Inhabited MACAddr

def Std.Net.instInhabitedMACAddr.default : MACAddr

def Std.Net.instDecidableEqMACAddr.decEq (x✝ x✝¹ : MACAddr) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Std.Net.instDecidableEqMACAddr : DecidableEq MACAddr

structure Std.Net.IPv4Addr : Type

Representation of an IPv4 address.

• octets : Vector UInt8 4

  This structure represents the address: octets[0].octets[1].octets[2].octets[3].

def Std.Net.instInhabitedIPv4Addr.default : IPv4Addr

@[implicit_reducible]

instance Std.Net.instInhabitedIPv4Addr : Inhabited IPv4Addr

def Std.Net.instDecidableEqIPv4Addr.decEq (x✝ x✝¹ : IPv4Addr) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Std.Net.instDecidableEqIPv4Addr : DecidableEq IPv4Addr

structure Std.Net.SocketAddressV4 : Type

A pair of an IPv4Addr and a port.

• addr : IPv4Addr
• port : UInt16

@[implicit_reducible]

instance Std.Net.instInhabitedSocketAddressV4 : Inhabited SocketAddressV4

def Std.Net.instInhabitedSocketAddressV4.default : SocketAddressV4

def Std.Net.instDecidableEqSocketAddressV4.decEq (x✝ x✝¹ : SocketAddressV4) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Std.Net.instDecidableEqSocketAddressV4 : DecidableEq SocketAddressV4

structure Std.Net.IPv6Addr : Type

Representation of an IPv6 address.

• segments : Vector UInt16 8

  This structure represents the address: segments[0]:segments[1]:....

@[implicit_reducible]

instance Std.Net.instInhabitedIPv6Addr : Inhabited IPv6Addr

def Std.Net.instInhabitedIPv6Addr.default : IPv6Addr

def Std.Net.instDecidableEqIPv6Addr.decEq (x✝ x✝¹ : IPv6Addr) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Std.Net.instDecidableEqIPv6Addr : DecidableEq IPv6Addr

structure Std.Net.SocketAddressV6 : Type

A pair of an IPv6Addr and a port.

• addr : IPv6Addr
• port : UInt16

@[implicit_reducible]

instance Std.Net.instInhabitedSocketAddressV6 : Inhabited SocketAddressV6

def Std.Net.instInhabitedSocketAddressV6.default : SocketAddressV6

@[implicit_reducible]

instance Std.Net.instDecidableEqSocketAddressV6 : DecidableEq SocketAddressV6

def Std.Net.instDecidableEqSocketAddressV6.decEq (x✝ x✝¹ : SocketAddressV6) : Decidable (x✝ = x✝¹)

inductive Std.Net.IPAddr : Type

An IP address, either IPv4 or IPv6.

• v4 (addr : IPv4Addr) : IPAddr
• v6 (addr : IPv6Addr) : IPAddr

def Std.Net.instInhabitedIPAddr.default : IPAddr

@[implicit_reducible]

instance Std.Net.instInhabitedIPAddr : Inhabited IPAddr

@[implicit_reducible]

instance Std.Net.instDecidableEqIPAddr : DecidableEq IPAddr

def Std.Net.instDecidableEqIPAddr.decEq (x✝ x✝¹ : IPAddr) : Decidable (x✝ = x✝¹)

inductive Std.Net.SocketAddress : Type

Either a SocketAddressV4 or SocketAddressV6.

• v4 (addr : SocketAddressV4) : SocketAddress
• v6 (addr : SocketAddressV6) : SocketAddress

@[implicit_reducible]

instance Std.Net.instInhabitedSocketAddress : Inhabited SocketAddress

def Std.Net.instInhabitedSocketAddress.default : SocketAddress

def Std.Net.instDecidableEqSocketAddress.decEq (x✝ x✝¹ : SocketAddress) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Std.Net.instDecidableEqSocketAddress : DecidableEq SocketAddress

inductive Std.Net.AddressFamily : Type

The kinds of address families supported by Lean, currently only IP variants.

• ipv4 : AddressFamily
• ipv6 : AddressFamily

@[implicit_reducible]

instance Std.Net.instInhabitedAddressFamily : Inhabited AddressFamily

def Std.Net.instInhabitedAddressFamily.default : AddressFamily

@[implicit_reducible]

instance Std.Net.instDecidableEqAddressFamily : DecidableEq AddressFamily

def Std.Net.IPv4Addr.ofParts (a b c d : UInt8) : IPv4Addr

Build the IPv4 address a.b.c.d.

@[extern lean_uv_pton_v4]

opaque Std.Net.IPv4Addr.ofString (s : String) : Option IPv4Addr

Try to parse s as an IPv4 address, returning none on failure.

@[extern lean_uv_ntop_v4]

opaque Std.Net.IPv4Addr.toString (addr : IPv4Addr) : String

Turn addr into a String in the usual IPv4 format.

@[implicit_reducible]

instance Std.Net.IPv4Addr.instToString : ToString IPv4Addr

@[implicit_reducible]

instance Std.Net.IPv4Addr.instCoeIPAddr : Coe IPv4Addr IPAddr

@[implicit_reducible]

instance Std.Net.SocketAddressV4.instCoeSocketAddress : Coe SocketAddressV4 SocketAddress

def Std.Net.IPv6Addr.ofParts (a b c d e f g h : UInt16) : IPv6Addr

Build the IPv6 address a:b:c:d:e:f:g:h.

@[extern lean_uv_pton_v6]

opaque Std.Net.IPv6Addr.ofString (s : String) : Option IPv6Addr

Try to parse s as an IPv6 address according to RFC 2373, returning none on failure.

@[extern lean_uv_ntop_v6]

opaque Std.Net.IPv6Addr.toString (addr : IPv6Addr) : String

Turn addr into a String in the IPv6 format described in RFC 2373.

@[implicit_reducible]

instance Std.Net.IPv6Addr.instToString : ToString IPv6Addr

@[implicit_reducible]

instance Std.Net.IPv6Addr.instCoeIPAddr : Coe IPv6Addr IPAddr

@[implicit_reducible]

instance Std.Net.SocketAddressV6.instCoeSocketAddress : Coe SocketAddressV6 SocketAddress

def Std.Net.IPAddr.family : IPAddr → AddressFamily

Obtain the AddressFamily associated with an IPAddr.

def Std.Net.IPAddr.toString : IPAddr → String

@[implicit_reducible]

instance Std.Net.IPAddr.instToString : ToString IPAddr

def Std.Net.SocketAddress.family : SocketAddress → AddressFamily

Obtain the AddressFamily associated with a SocketAddress.

def Std.Net.SocketAddress.ipAddr : SocketAddress → IPAddr

Obtain the IPAddr contained in a SocketAddress.

def Std.Net.SocketAddress.port : SocketAddress → UInt16

Obtain the port contained in a SocketAddress.

structure Std.Net.InterfaceAddress : Type

Represents an interface address, including details such as the interface name, whether it is internal, the associated address, and the network mask.

• name : String

  The name of the network interface.

• physicalAddress : MACAddr
• isLoopback : Bool

  Indicates whether the interface is a loopback interface.

• address : IPAddr

  The IP address assigned to the interface.

• netMask : IPAddr

  The subnet mask associated with the interface.

def Std.Net.instInhabitedInterfaceAddress.default : InterfaceAddress

@[implicit_reducible]

instance Std.Net.instInhabitedInterfaceAddress : Inhabited InterfaceAddress

@[implicit_reducible]

instance Std.Net.instDecidableEqInterfaceAddress : DecidableEq InterfaceAddress

def Std.Net.instDecidableEqInterfaceAddress.decEq (x✝ x✝¹ : InterfaceAddress) : Decidable (x✝ = x✝¹)

@[extern lean_uv_interface_addresses]

opaque Std.Net.interfaceAddresses : IO (Array InterfaceAddress)

Gets address information about the network interfaces on the system, including disabled ones and multiple addresses for each interface.