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 anIPv4Addr
or anIPv6Addr
.SocketAddress
: Can either be aSocketAddressV4
orSocketAddressV6
.
Representation of a MAC address.
This structure represents the address:
octets[0]:octets[1]:octets[2]:octets[3]:octets[4]:octets[5]
.
Instances For
Equations
Equations
- Std.Net.instInhabitedMACAddr.default = { octets := default }
Instances For
Representation of an IPv4 address.
This structure represents the address:
octets[0].octets[1].octets[2].octets[3]
.
Instances For
Equations
- Std.Net.instInhabitedIPv4Addr.default = { octets := default }
Instances For
Equations
Instances For
Equations
Instances For
Representation of an IPv6 address.
This structure represents the address:
segments[0]:segments[1]:...
.
Instances For
Equations
Equations
- Std.Net.instInhabitedIPv6Addr.default = { segments := default }
Instances For
Instances For
Equations
Instances For
Instances For
Equations
Equations
- Std.Net.instDecidableEqIPAddr.decEq (Std.Net.IPAddr.v4 a) (Std.Net.IPAddr.v4 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- Std.Net.instDecidableEqIPAddr.decEq (Std.Net.IPAddr.v4 addr) (Std.Net.IPAddr.v6 addr_1) = isFalse ⋯
- Std.Net.instDecidableEqIPAddr.decEq (Std.Net.IPAddr.v6 addr) (Std.Net.IPAddr.v4 addr_1) = isFalse ⋯
- Std.Net.instDecidableEqIPAddr.decEq (Std.Net.IPAddr.v6 a) (Std.Net.IPAddr.v6 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Instances For
Either a SocketAddressV4
or SocketAddressV6
.
- v4 (addr : SocketAddressV4) : SocketAddress
- v6 (addr : SocketAddressV6) : SocketAddress
Instances For
Equations
Equations
- Std.Net.instDecidableEqSocketAddress.decEq (Std.Net.SocketAddress.v4 a) (Std.Net.SocketAddress.v4 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- Std.Net.instDecidableEqSocketAddress.decEq (Std.Net.SocketAddress.v4 addr) (Std.Net.SocketAddress.v6 addr_1) = isFalse ⋯
- Std.Net.instDecidableEqSocketAddress.decEq (Std.Net.SocketAddress.v6 addr) (Std.Net.SocketAddress.v4 addr_1) = isFalse ⋯
- Std.Net.instDecidableEqSocketAddress.decEq (Std.Net.SocketAddress.v6 a) (Std.Net.SocketAddress.v6 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Instances For
The kinds of address families supported by Lean, currently only IP variants.
- ipv4 : AddressFamily
- ipv6 : AddressFamily
Instances For
Equations
Try to parse s
as an IPv4 address, returning none
on failure.
Equations
- Std.Net.IPv4Addr.instToString = { toString := Std.Net.IPv4Addr.toString }
Equations
- Std.Net.IPv4Addr.instCoeIPAddr = { coe := fun (addr : Std.Net.IPv4Addr) => Std.Net.IPAddr.v4 addr }
Equations
- Std.Net.SocketAddressV4.instCoeSocketAddress = { coe := fun (addr : Std.Net.SocketAddressV4) => Std.Net.SocketAddress.v4 addr }
Equations
- Std.Net.IPv6Addr.instToString = { toString := Std.Net.IPv6Addr.toString }
Equations
- Std.Net.IPv6Addr.instCoeIPAddr = { coe := fun (addr : Std.Net.IPv6Addr) => Std.Net.IPAddr.v6 addr }
Equations
- Std.Net.SocketAddressV6.instCoeSocketAddress = { coe := fun (addr : Std.Net.SocketAddressV6) => Std.Net.SocketAddress.v6 addr }
Equations
- (Std.Net.IPAddr.v4 addr).toString = addr.toString
- (Std.Net.IPAddr.v6 addr).toString = addr.toString
Instances For
Equations
- Std.Net.IPAddr.instToString = { toString := Std.Net.IPAddr.toString }
Obtain the IPAddr
contained in a SocketAddress
.
Equations
- (Std.Net.SocketAddress.v4 addr).ipAddr = Std.Net.IPAddr.v4 addr.addr
- (Std.Net.SocketAddress.v6 addr).ipAddr = Std.Net.IPAddr.v6 addr.addr
Instances For
Obtain the port contained in a SocketAddress
.
Equations
- (Std.Net.SocketAddress.v4 addr).port = addr.port
- (Std.Net.SocketAddress.v6 addr).port = addr.port
Instances For
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.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Gets address information about the network interfaces on the system, including disabled ones and multiple addresses for each interface.