def LeanUri.Internal.decOctet : Std.Internal.Parsec.String.Parser Nat

dec-octet = DIGIT / %x31-39 DIGIT / "1" 2DIGIT / "2" %x30-34 DIGIT / "25" %x30-35

Equations

• LeanUri.Internal.decOctet = do let n ← Std.Internal.Parsec.String.digits if n > 255 then Std.Internal.Parsec.fail (toString "decimal octet out of range: " ++ toString n) else pure n

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

IPv4address = dec-octet "." dec-octet "." dec-octet "." dec-octet

Equations

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