@[inline]

def System.Uri.UriEscape.zero : UInt8

Equations

• System.Uri.UriEscape.zero = Nat.toUInt8 (Char.toNat (Char.ofNat 48))

@[inline]

def System.Uri.UriEscape.nine : UInt8

Equations

• System.Uri.UriEscape.nine = Nat.toUInt8 (Char.toNat (Char.ofNat 57))

@[inline]

def System.Uri.UriEscape.lettera : UInt8

Equations

• System.Uri.UriEscape.lettera = Nat.toUInt8 (Char.toNat (Char.ofNat 97))

@[inline]

def System.Uri.UriEscape.letterf : UInt8

Equations

• System.Uri.UriEscape.letterf = Nat.toUInt8 (Char.toNat (Char.ofNat 102))

@[inline]

def System.Uri.UriEscape.letterA : UInt8

Equations

• System.Uri.UriEscape.letterA = Nat.toUInt8 (Char.toNat (Char.ofNat 65))

@[inline]

def System.Uri.UriEscape.letterF : UInt8

Equations

• System.Uri.UriEscape.letterF = Nat.toUInt8 (Char.toNat (Char.ofNat 70))

def System.Uri.UriEscape.decodeUri (uri : String) : String

Decode %HH escapings in the given string. Note that sometimes a consecutive sequence of multiple escapings can represent a utf-8 encoded sequence for a single unicode code point and these will also be decoded correctly.

Equations

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

def System.Uri.UriEscape.decodeUri.hexDigitToUInt8? (c : UInt8) : Option UInt8

Equations

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

def System.Uri.UriEscape.rfc3986ReservedChars : List Char

Equations

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

def System.Uri.UriEscape.uriEscapeAsciiChar (c : Char) : String

Equations

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

def System.Uri.UriEscape.uriEscapeAsciiChar.uInt8ToHex (c : UInt8) : String

Equations

• System.Uri.UriEscape.uriEscapeAsciiChar.uInt8ToHex c = let d2 := c / 16; let d1 := c % 16; String.toUpper (hexDigitRepr (UInt8.toNat d2) ++ hexDigitRepr (UInt8.toNat d1))

def System.Uri.escapeUri (uri : String) : String

Replaces special characters in the given Uri with %HH Uri escapings.

Equations

• System.Uri.escapeUri uri = String.foldl (fun (s : String) (c : Char) => s ++ System.Uri.UriEscape.uriEscapeAsciiChar c) "" uri

def System.Uri.unescapeUri (s : String) : String

Replaces all %HH Uri escapings in the given string with their corresponding unicode code points. Note that sometimes a consecutive sequence of multiple escapings can represent a utf-8 encoded sequence for a single unicode code point and these will also be decoded correctly.

Equations

• System.Uri.unescapeUri s = System.Uri.UriEscape.decodeUri s

def System.Uri.pathToUri (fname : Lake.FilePath) : String

Convert the given FilePath to a "file:///encodedpath" Uri.

Equations

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

def System.Uri.fileUriToPath? (uri : String) : Option Lake.FilePath

Convert the given uri to a FilePath stripping the 'file://' prefix, ignoring the optional host name.

Equations

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