Idris2Doc : HTTP.URI

HTTP.URI

(source)

Definitions

data QueryVal : Type
Totality: total
Visibility: public export
Constructors:
QVal : ByteString -> QueryVal
QEmpty : QueryVal

Hints:
Eq QueryVal
Show QueryVal
0 Queries : Type
Totality: total
Visibility: public export
record URI : Type
  -- TODO: Special treatment of user info

Totality: total
Visibility: public export
Constructor: 
MkURI : Maybe ByteString -> Maybe ByteString -> Bool -> List ByteString -> Queries -> Maybe ByteString -> URI

Projections:
.abs : URI -> Bool
.authority : URI -> Maybe ByteString
.fragment : URI -> Maybe ByteString
.path : URI -> List ByteString
.queries : URI -> Queries
.scheme : URI -> Maybe ByteString

Hints:
Eq URI
Interpolation URI
Show URI
.scheme : URI -> Maybe ByteString
Totality: total
Visibility: public export
scheme : URI -> Maybe ByteString
Totality: total
Visibility: public export
.authority : URI -> Maybe ByteString
Totality: total
Visibility: public export
authority : URI -> Maybe ByteString
Totality: total
Visibility: public export
.abs : URI -> Bool
Totality: total
Visibility: public export
abs : URI -> Bool
Totality: total
Visibility: public export
.path : URI -> List ByteString
Totality: total
Visibility: public export
path : URI -> List ByteString
Totality: total
Visibility: public export
.queries : URI -> Queries
Totality: total
Visibility: public export
queries : URI -> Queries
Totality: total
Visibility: public export
.fragment : URI -> Maybe ByteString
Totality: total
Visibility: public export
fragment : URI -> Maybe ByteString
Totality: total
Visibility: public export
encodePath : URI -> ByteString
Totality: total
Visibility: export
encodeURI : URI -> ByteString
  Properly escapes characters in a URL if necessary and
combines the different parts in the URI.

Totality: total
Visibility: export
parseURI : Origin -> ByteString -> Either (ParseError Void) URI
Totality: total
Visibility: export
testParseURI : ByteString -> IO ()
Totality: total
Visibility: export