@[inline]

def System.Uri.UriEscape.zero : UInt8

Equations

• System.Uri.UriEscape.zero = '0'.toNat.toUInt8

@[inline]

def System.Uri.UriEscape.nine : UInt8

Equations

• System.Uri.UriEscape.nine = '9'.toNat.toUInt8

@[inline]

def System.Uri.UriEscape.lettera : UInt8

Equations

• System.Uri.UriEscape.lettera = 'a'.toNat.toUInt8

@[inline]

def System.Uri.UriEscape.letterf : UInt8

Equations

• System.Uri.UriEscape.letterf = 'f'.toNat.toUInt8

@[inline]

def System.Uri.UriEscape.letterA : UInt8

Equations

• System.Uri.UriEscape.letterA = 'A'.toNat.toUInt8

@[inline]

def System.Uri.UriEscape.letterF : UInt8

Equations

• System.Uri.UriEscape.letterF = 'F'.toNat.toUInt8

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

• System.Uri.UriEscape.rfc3986ReservedChars = [';', ':', '?', '#', '[', ']', '@', '&', '=', '+', '$', ',', '!', ''', '(', ')', '*', '%', ' ']

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; (hexDigitRepr d2.toNat ++ hexDigitRepr d1.toNat).toUpper

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.