def LeanUri.Internal.h16 : Std.Internal.Parsec.String.Parser String

h16 = 1*4HEXDIG (16 bits of address in hexadecimal)

Equations

• One or more equations did not get rendered due to their size.

def LeanUri.Internal.ls32 : Std.Internal.Parsec.String.Parser String

ls32 = ( h16 ":" h16 ) / IPv4address (least-significant 32 bits)

Equations

• One or more equations did not get rendered due to their size.

def LeanUri.Internal.h16Colon : Std.Internal.Parsec.String.Parser String

Helper to parse n repetitions of h16 followed by colon

Equations

• LeanUri.Internal.h16Colon = do let h ← LeanUri.Internal.h16 Std.Internal.Parsec.String.skipChar ':' pure (h ++ ":")

def LeanUri.Internal.nH16Colon (n : Nat) : Std.Internal.Parsec.String.Parser String

Parse exactly n h16 groups with trailing colons

Equations

• LeanUri.Internal.nH16Colon n = do let parts ← List.mapM (fun (x : Nat) => LeanUri.Internal.h16Colon) (List.range n) pure (String.join parts)

def LeanUri.Internal.optPrefix (maxGroups : Nat) : Std.Internal.Parsec.String.Parser String

Parse optional prefix: up to n h16 groups with colons, then one h16 without colon

Equations

• One or more equations did not get rendered due to their size.

def LeanUri.Internal.ipv6address : Std.Internal.Parsec.String.Parser String

IPv6address with all 9 variations from RFC 3986

Equations

• One or more equations did not get rendered due to their size.

def LeanUri.Internal.ipvFuture : Std.Internal.Parsec.String.Parser String

Equations

• One or more equations did not get rendered due to their size.

def LeanUri.Internal.ipLiteral : Std.Internal.Parsec.String.Parser String

IP-literal = "[" ( IPv6address / IPvFuture ) "]"

Equations

• One or more equations did not get rendered due to their size.