Network.HTTP.URL

Definitions

record Hostname : Type

Totality: total
Visibility: public export
Constructor: 

MkHostname : String -> Maybe Bits16 -> Hostname

Projections:

.domain : Hostname -> String

.port : Hostname -> Maybe Bits16

Hints:

Eq Hostname

Show Hostname

.domain : Hostname -> String

Visibility: public export

domain : Hostname -> String

Visibility: public export

.port : Hostname -> Maybe Bits16

Visibility: public export

port : Hostname -> Maybe Bits16

Visibility: public export

record URLCredential : Type

Totality: total
Visibility: public export
Constructor: 

MkURLCredential : String -> Maybe String -> URLCredential

Projections:

.password : URLCredential -> Maybe String

.username : URLCredential -> String

Hints:

Eq URLCredential

Show URLCredential

.username : URLCredential -> String

Visibility: public export

username : URLCredential -> String

Visibility: public export

.password : URLCredential -> Maybe String

Visibility: public export

password : URLCredential -> Maybe String

Visibility: public export

record URL : Type

Totality: total
Visibility: public export
Constructor: 

MkURL : String -> Maybe URLCredential -> Hostname -> Path -> String -> URL

Projections:

.credential : URL -> Maybe URLCredential

.extensions : URL -> String

.host : URL -> Hostname

.path : URL -> Path

.protocol : URL -> String

Hint: 

Show URL

.protocol : URL -> String

Visibility: public export

protocol : URL -> String

Visibility: public export

.credential : URL -> Maybe URLCredential

Visibility: public export

credential : URL -> Maybe URLCredential

Visibility: public export

.host : URL -> Hostname

Visibility: public export

host : URL -> Hostname

Visibility: public export

.path : URL -> Path

Visibility: public export

path : URL -> Path

Visibility: public export

.extensions : URL -> String

Visibility: public export

extensions : URL -> String

Visibility: public export

parse_url : Parser URL

Visibility: export

url_from_string : String -> Either String URL

Visibility: export

data URLProof : AsList m -> Type

Totality: total
Visibility: public export
Constructors:

IsHTTPURL : URLProof ('h' :: Delay ('t' :: Delay ('t' :: Delay ('p' :: Delay (':' :: Delay ('/' :: Delay ('/' :: xs)))))))

IsHTTPSURL : URLProof ('h' :: Delay ('t' :: Delay ('t' :: Delay ('p' :: Delay ('s' :: Delay (':' :: Delay ('/' :: Delay ('/' :: xs))))))))

url' : (str : String) -> {auto 0 _ : URLProof (asList str)} -> URL

Visibility: export

add : URL -> String -> URL

Visibility: export

parse_hostname : String -> Either String Hostname

Visibility: export

hostname_string : Hostname -> String

Visibility: export

url_port_number : URL -> Maybe Bits16

Visibility: export