Documentation

Std.Net.Addr

This module contains Lean representations of IP and socket addresses:

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].

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

      Representation of an IPv4 address.

      • octets : Vector UInt8 4

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

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

          A pair of an IPv4Addr and a port.

          Instances For
            Equations
            Instances For

              Representation of an IPv6 address.

              • segments : Vector UInt16 8

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

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

                  A pair of an IPv6Addr and a port.

                  Instances For
                    Equations
                    Instances For
                      inductive Std.Net.IPAddr :

                      An IP address, either IPv4 or IPv6.

                      Instances For

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

                        Instances For

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

                          Equations
                          Instances For
                            @[extern lean_uv_pton_v4]

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

                            @[extern lean_uv_ntop_v4]

                            Turn addr into a String in the usual IPv4 format.

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

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

                            Equations
                            Instances For
                              @[extern lean_uv_pton_v6]

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

                              @[extern lean_uv_ntop_v6]

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

                              Obtain the port contained in a SocketAddress.

                              Equations
                              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
                                      @[extern lean_uv_interface_addresses]

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