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

userinfo = *( unreserved / pct-encoded / sub-delims / ":" )

Equations

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

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

port = *DIGIT

Equations

• LeanUri.Internal.port = Std.Internal.Parsec.manyChars Std.Internal.Parsec.String.digit

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

host = IP-literal / IPv4address / reg-name

Equations

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

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

Equations

• LeanUri.Internal.host = (Std.Internal.Parsec.attempt LeanUri.Internal.ipLiteral <|> Std.Internal.Parsec.attempt LeanUri.Internal.ipv4address <|> LeanUri.Internal.regName)

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

authority = [ userinfo "@" ] host [ ":" port ]

Equations

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

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

pchar = unreserved / pct-encoded / sub-delims / ":" / "@"

Equations

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

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

segment = *pchar

Equations

• LeanUri.Internal.segment = LeanUri.Internal.manyStrings LeanUri.Internal.pchar

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

segment-nz = 1*pchar (non-zero-length segment)

Equations

• LeanUri.Internal.segmentNz = do let first ← LeanUri.Internal.pchar let rest ← LeanUri.Internal.manyStrings LeanUri.Internal.pchar pure (first ++ rest)

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

segment-nz-nc = 1*( unreserved / pct-encoded / sub-delims / "@" ) (non-zero-length segment without any colon ":")

Equations

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

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

path-abempty = *( "/" segment )

Equations

• LeanUri.Internal.pathAbempty = LeanUri.Internal.manyStrings do let s ← Std.Internal.Parsec.String.pstring "/" *> LeanUri.Internal.segment pure ("/" ++ s)

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

path-absolute = "/" [ segment-nz *( "/" segment ) ]

Equations

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

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

path-noscheme = segment-nz-nc *( "/" segment )

Equations

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

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

path-rootless = segment-nz *( "/" segment )

Equations

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

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

path-empty = 0<pchar>

Equations

• LeanUri.Internal.pathEmpty = pure ""

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

query = *( pchar / "/" / "?" )

Equations

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

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

fragment = *( pchar / "/" / "?" )

Equations

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

def LeanUri.Internal.hierPart : Std.Internal.Parsec.String.Parser (Option String × String)

hier-part = "//" authority path-abempty / path-absolute / path-rootless / path-empty

Equations

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

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

scheme = ALPHA *( ALPHA / DIGIT / "+" / "-" / "." )

Equations

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

def LeanUri.Internal.uri : Std.Internal.Parsec.String.Parser URI

URI = scheme ":" hier-part [ "?" query ] [ "#" fragment ]

Equations

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

def LeanUri.Internal.relativePart : Std.Internal.Parsec.String.Parser (Option String × String)

relative-part = "//" authority path-abempty / path-absolute / path-noscheme / path-empty

Equations

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

def LeanUri.Internal.relativeRef : Std.Internal.Parsec.String.Parser RelativeRef

relative-ref = relative-part [ "?" query ] [ "#" fragment ]

Equations

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

Reference Resolution (RFC 3986 Section 5.2)

partial def LeanUri.Internal.removeDotSegments (input : String) (output : String := "") : String

def LeanUri.Internal.mergePaths (basePath refPath : String) (baseHasAuth : Bool) : String

Equations

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

def LeanUri.Internal.resolve (base : URI) (ref : RelativeRef) : URI

Equations

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

def LeanUri.Internal.uriReference : Std.Internal.Parsec.String.Parser (URI ⊕ RelativeRef)

Equations

• LeanUri.Internal.uriReference = ((do let u ← LeanUri.Internal.uri pure (Sum.inl u)).attempt <|> do let r ← LeanUri.Internal.relativeRef pure (Sum.inr r))

def LeanUri.Internal.parseAndResolve (baseUri : URI) (reference : String) : Except String URI

Equations

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