inductive Network.HTTP.Req.Scheme : Type

URL scheme, used as a phantom parameter on Url and Option to enforce HTTPS-only constraints at the type level. $$\text{Scheme} = \text{Http} \mid \text{Https}$$

• Http : Scheme
• Https : Scheme

def Network.HTTP.Req.instBEqScheme.beq : Scheme → Scheme → Bool

Equations

• Network.HTTP.Req.instBEqScheme.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Network.HTTP.Req.instBEqScheme : BEq Scheme

Equations

• Network.HTTP.Req.instBEqScheme = { beq := Network.HTTP.Req.instBEqScheme.beq }

@[implicit_reducible]

instance Network.HTTP.Req.instDecidableEqScheme : DecidableEq Scheme

Equations

• Network.HTTP.Req.instDecidableEqScheme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Network.HTTP.Req.instReprScheme.repr : Scheme → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.HTTP.Req.instReprScheme : Repr Scheme

Equations

• Network.HTTP.Req.instReprScheme = { reprPrec := Network.HTTP.Req.instReprScheme.repr }

theorem Network.HTTP.Req.Scheme.http_ne_https : Http ≠ Https

HTTP and HTTPS schemes are distinct (enables auth separation).

structure Network.HTTP.Req.Url (scheme : Scheme) : Type

A correct-by-construction URL parameterized by scheme.

The scheme phantom parameter enables HTTPS-only auth enforcement. Hostname is proven non-empty by construction. Path segments are stored in order.

$$\text{Url}\ s = \{ \text{host} : \{h : \text{String} \mid h.\text{length} > 0\},\; \text{segments} : \text{List String} \}$$

• host : String

  The hostname. Must be non-empty (enforced by proof).

• segments : List String

  Path segments (e.g., ["api", "v1", "users"]).

• host_nonempty : self.host.length > 0

  Host is non-empty (proof, erased at runtime).

@[implicit_reducible]

instance Network.HTTP.Req.instReprUrl {s : Scheme} : Repr (Url s)

Equations

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

def Network.HTTP.Req.http (host : String) (h : host.length > 0 := by decide) : Url Scheme.Http

Construct an HTTP URL from a hostname. $$\text{http} : \text{String} \to \text{Url .Http}$$

Equations

• Network.HTTP.Req.http host h = { host := host, host_nonempty := h }

def Network.HTTP.Req.https (host : String) (h : host.length > 0 := by decide) : Url Scheme.Https

Construct an HTTPS URL from a hostname. $$\text{https} : \text{String} \to \text{Url .Https}$$

Equations

• Network.HTTP.Req.https host h = { host := host, host_nonempty := h }

def Network.HTTP.Req.Url.append {s : Scheme} (url : Url s) (segment : String) : Url s

Append a path segment to a URL. $$(\text{/:}) : \text{Url}\ s \to \text{String} \to \text{Url}\ s$$

Equations

• url /: segment = { host := url.host, segments := url.segments ++ [segment], host_nonempty := ⋯ }

def Network.HTTP.Req.«term_/:_» : Lean.TrailingParserDescr

Infix operator for path segments: https "api.example.com" /: "v1" /: "users"

Equations

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

def Network.HTTP.Req.Url.path {s : Scheme} (url : Url s) : String

Render a URL's path component (with leading /).

Equations

• url.path = if url.segments.isEmpty = true then "/" else "/" ++ "/".intercalate url.segments

def Network.HTTP.Req.Url.defaultPort {s : Scheme} : Url s → UInt16

Get the default port for a URL based on its scheme.

Equations

• x_1.defaultPort = 80
• x_1.defaultPort = 443

def Network.HTTP.Req.Url.isSecure {s : Scheme} : Url s → Bool

Whether the URL scheme is secure (HTTPS).

Equations

• x_1.isSecure = false
• x_1.isSecure = true

inductive Network.HTTP.Req.CanHaveBody : Type

Whether an HTTP method allows a request body. $$\text{CanHaveBody} = \text{YesBody} \mid \text{NoBody}$$

• YesBody : CanHaveBody
• NoBody : CanHaveBody

@[implicit_reducible]

instance Network.HTTP.Req.instBEqCanHaveBody : BEq CanHaveBody

Equations

• Network.HTTP.Req.instBEqCanHaveBody = { beq := Network.HTTP.Req.instBEqCanHaveBody.beq }

def Network.HTTP.Req.instBEqCanHaveBody.beq : CanHaveBody → CanHaveBody → Bool

Equations

• Network.HTTP.Req.instBEqCanHaveBody.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Network.HTTP.Req.instDecidableEqCanHaveBody : DecidableEq CanHaveBody

Equations

• Network.HTTP.Req.instDecidableEqCanHaveBody x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Network.HTTP.Req.instReprCanHaveBody.repr : CanHaveBody → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.HTTP.Req.instReprCanHaveBody : Repr CanHaveBody

Equations

• Network.HTTP.Req.instReprCanHaveBody = { reprPrec := Network.HTTP.Req.instReprCanHaveBody.repr }

class Network.HTTP.Req.HttpMethod (m : Type) : Type

Typeclass for HTTP methods. Maps each method to its body permission and wire name. $$\text{HttpMethod}\ m = \{ \text{allowsBody} : \text{CanHaveBody},\; \text{methodName} : \text{String} \}$$

• allowsBody : CanHaveBody

  Whether this method allows a request body.

• methodName : String

  The HTTP method name as it appears on the wire (e.g., "GET").

class Network.HTTP.Req.HttpBody (b : Type) : Type

Typeclass for HTTP request bodies. Maps each body type to its content and content-type. $$\text{HttpBody}\ b = \{ \text{providesBody} : \text{CanHaveBody},\; \text{getBody} : b \to \text{Option ByteArray},\; \text{getContentType} : b \to \text{Option String} \}$$

• providesBody : CanHaveBody

  Whether this body type provides a body.

• getBody : b → Option ByteArray

  Get the body bytes. none means no body.

• getContentType : b → Option String

  Get the Content-Type header value.

class Network.HTTP.Req.HttpBodyAllowed (allows provides : CanHaveBody) : Type

Compile-time constraint: method/body compatibility.

This typeclass has instances for all valid combinations:

• (.YesBody, .YesBody) — POST with body
• (.YesBody, .NoBody) — POST with no body (allowed)
• (.NoBody, .NoBody) — GET with no body

The missing instance (.NoBody, .YesBody) means that req GET url (ReqBodyBs data) ... fails at compile time with "failed to synthesize HttpBodyAllowed .NoBody .YesBody".

@[implicit_reducible]

instance Network.HTTP.Req.instHttpBodyAllowedYesBody : HttpBodyAllowed CanHaveBody.YesBody CanHaveBody.YesBody

Equations

• Network.HTTP.Req.instHttpBodyAllowedYesBody = { }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpBodyAllowedYesBodyNoBody : HttpBodyAllowed CanHaveBody.YesBody CanHaveBody.NoBody

Equations

• Network.HTTP.Req.instHttpBodyAllowedYesBodyNoBody = { }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpBodyAllowedNoBody : HttpBodyAllowed CanHaveBody.NoBody CanHaveBody.NoBody

Equations

• Network.HTTP.Req.instHttpBodyAllowedNoBody = { }

structure Network.HTTP.Req.GET : Type

HTTP GET method. Does not allow a request body.

structure Network.HTTP.Req.POST : Type

HTTP POST method. Allows a request body.

structure Network.HTTP.Req.HEAD : Type

HTTP HEAD method. Does not allow a request body.

structure Network.HTTP.Req.PUT : Type

HTTP PUT method. Allows a request body.

structure Network.HTTP.Req.DELETE : Type

HTTP DELETE method. Does not allow a request body (matches Haskell req).

structure Network.HTTP.Req.PATCH : Type

HTTP PATCH method. Allows a request body.

structure Network.HTTP.Req.OPTIONS : Type

HTTP OPTIONS method. Does not allow a request body.

structure Network.HTTP.Req.TRACE : Type

HTTP TRACE method. Does not allow a request body.

structure Network.HTTP.Req.CONNECT : Type

HTTP CONNECT method. Does not allow a request body.

@[implicit_reducible]

instance Network.HTTP.Req.instHttpMethodGET : HttpMethod GET

Equations

• Network.HTTP.Req.instHttpMethodGET = { allowsBody := Network.HTTP.Req.CanHaveBody.NoBody, methodName := "GET" }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpMethodPOST : HttpMethod POST

Equations

• Network.HTTP.Req.instHttpMethodPOST = { allowsBody := Network.HTTP.Req.CanHaveBody.YesBody, methodName := "POST" }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpMethodHEAD : HttpMethod HEAD

Equations

• Network.HTTP.Req.instHttpMethodHEAD = { allowsBody := Network.HTTP.Req.CanHaveBody.NoBody, methodName := "HEAD" }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpMethodPUT : HttpMethod PUT

Equations

• Network.HTTP.Req.instHttpMethodPUT = { allowsBody := Network.HTTP.Req.CanHaveBody.YesBody, methodName := "PUT" }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpMethodDELETE : HttpMethod DELETE

Equations

• Network.HTTP.Req.instHttpMethodDELETE = { allowsBody := Network.HTTP.Req.CanHaveBody.NoBody, methodName := "DELETE" }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpMethodPATCH : HttpMethod PATCH

Equations

• Network.HTTP.Req.instHttpMethodPATCH = { allowsBody := Network.HTTP.Req.CanHaveBody.YesBody, methodName := "PATCH" }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpMethodOPTIONS : HttpMethod OPTIONS

Equations

• Network.HTTP.Req.instHttpMethodOPTIONS = { allowsBody := Network.HTTP.Req.CanHaveBody.NoBody, methodName := "OPTIONS" }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpMethodTRACE : HttpMethod TRACE

Equations

• Network.HTTP.Req.instHttpMethodTRACE = { allowsBody := Network.HTTP.Req.CanHaveBody.NoBody, methodName := "TRACE" }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpMethodCONNECT : HttpMethod CONNECT

Equations

• Network.HTTP.Req.instHttpMethodCONNECT = { allowsBody := Network.HTTP.Req.CanHaveBody.NoBody, methodName := "CONNECT" }

theorem Network.HTTP.Req.get_no_body : HttpMethod.allowsBody GET = CanHaveBody.NoBody

theorem Network.HTTP.Req.post_yes_body : HttpMethod.allowsBody POST = CanHaveBody.YesBody

theorem Network.HTTP.Req.put_yes_body : HttpMethod.allowsBody PUT = CanHaveBody.YesBody

theorem Network.HTTP.Req.patch_yes_body : HttpMethod.allowsBody PATCH = CanHaveBody.YesBody

theorem Network.HTTP.Req.head_no_body : HttpMethod.allowsBody HEAD = CanHaveBody.NoBody

theorem Network.HTTP.Req.delete_no_body : HttpMethod.allowsBody DELETE = CanHaveBody.NoBody

structure Network.HTTP.Req.NoReqBody : Type

No request body. Used with GET, HEAD, DELETE, etc.

@[implicit_reducible]

instance Network.HTTP.Req.instHttpBodyNoReqBody : HttpBody NoReqBody

Equations

• Network.HTTP.Req.instHttpBodyNoReqBody = { providesBody := Network.HTTP.Req.CanHaveBody.NoBody, getBody := fun (x : Network.HTTP.Req.NoReqBody) => none }

structure Network.HTTP.Req.ReqBodyBs : Type

Strict ByteArray body. Sets Content-Type to application/octet-stream.

• bytes : ByteArray

@[implicit_reducible]

instance Network.HTTP.Req.instHttpBodyReqBodyBs : HttpBody ReqBodyBs

Equations

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

structure Network.HTTP.Req.ReqBodyLbs : Type

Lazy ByteArray body (same as strict for now; lazy distinction is for API compatibility).

• bytes : ByteArray

@[implicit_reducible]

instance Network.HTTP.Req.instHttpBodyReqBodyLbs : HttpBody ReqBodyLbs

Equations

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

structure Network.HTTP.Req.ReqBodyUrlEnc : Type

URL-encoded form body (application/x-www-form-urlencoded).

• params : List (String × String)

@[implicit_reducible]

instance Network.HTTP.Req.instHttpBodyReqBodyUrlEnc : HttpBody ReqBodyUrlEnc

Equations

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

structure Network.HTTP.Req.ReqBodyFile : Type

File body. Reads the file at send time.

• path : String

@[implicit_reducible]

instance Network.HTTP.Req.instHttpBodyReqBodyFile : HttpBody ReqBodyFile

Equations

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

class Network.HTTP.Req.HttpResponse (r : Type) : Type

Typeclass for HTTP response interpretation. Defines how to parse the raw Network.HTTP.Client.Response into a typed response value. $$\text{HttpResponse}\ r = \{ \text{interpretResponse} : \text{Response} \to \text{IO}\ r,\; \text{acceptHeader} : \text{Option String} \}$$

• interpretResponse : Client.Response → IO r

  Parse a raw HTTP response into the typed response.

• acceptHeader : Option String

  Optional Accept header value to send with the request.

structure Network.HTTP.Req.IgnoreResponse : Type

Ignore the response body. Only status and headers are returned.

• status : Types.Status

  Response status.

• headers : Types.ResponseHeaders

  Response headers.

def Network.HTTP.Req.instReprIgnoreResponse.repr : IgnoreResponse → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.HTTP.Req.instReprIgnoreResponse : Repr IgnoreResponse

Equations

• Network.HTTP.Req.instReprIgnoreResponse = { reprPrec := Network.HTTP.Req.instReprIgnoreResponse.repr }

@[implicit_reducible]

instance Network.HTTP.Req.instHttpResponseIgnoreResponse : HttpResponse IgnoreResponse

Equations

• Network.HTTP.Req.instHttpResponseIgnoreResponse = { interpretResponse := fun (resp : Network.HTTP.Client.Response) => pure { status := resp.statusCode, headers := resp.headers } }

structure Network.HTTP.Req.BsResponse : Type

Strict ByteArray response — returns the full body as a ByteArray.

• status : Types.Status

  Response status.

• headers : Types.ResponseHeaders

  Response headers.

• body : ByteArray

  Response body.

@[implicit_reducible]

instance Network.HTTP.Req.instHttpResponseBsResponse : HttpResponse BsResponse

Equations

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

def Network.HTTP.Req.ignoreResponse : IgnoreResponse

Select IgnoreResponse as the response type.

Equations

• Network.HTTP.Req.ignoreResponse = { status := Network.HTTP.Types.status200, headers := [] }

def Network.HTTP.Req.bsResponse : BsResponse

Select BsResponse as the response type.

Equations

• Network.HTTP.Req.bsResponse = { status := Network.HTTP.Types.status200, headers := [], body := ByteArray.empty }

structure Network.HTTP.Req.ReqOption (scheme : Scheme) : Type

Composable request options, parameterized by scheme.

Forms a Monoid via Append / EmptyCollection. The scheme phantom parameter enables HTTPS-only authentication enforcement: basicAuth returns ReqOption .Https, so it can only be passed to req when the URL is also Url .Https.

$$\text{ReqOption}\ s = \{ \text{extraHeaders},\; \text{queryParams},\; \text{portOverride},\; \text{timeout} \}$$

• extraHeaders : Types.RequestHeaders

  Extra headers to add to the request.

• queryParams : List (String × String)

  Extra query parameters (key, value).

• portOverride : Option UInt16

  Override the default port.

• timeout : Option Nat

  Response timeout in milliseconds.

@[implicit_reducible]

instance Network.HTTP.Req.instReprReqOption {scheme✝ : Scheme} : Repr (ReqOption scheme✝)

Equations

• Network.HTTP.Req.instReprReqOption = { reprPrec := Network.HTTP.Req.instReprReqOption.repr }

def Network.HTTP.Req.instReprReqOption.repr {scheme✝ : Scheme} : ReqOption scheme✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.HTTP.Req.instAppendReqOption {s : Scheme} : Append (ReqOption s)

Equations

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

@[implicit_reducible]

instance Network.HTTP.Req.instEmptyCollectionReqOption {s : Scheme} : EmptyCollection (ReqOption s)

Equations

• Network.HTTP.Req.instEmptyCollectionReqOption = { emptyCollection := { } }

theorem Network.HTTP.Req.option_extraHeaders_append_assoc {s : Scheme} (a b c : ReqOption s) : (a ++ b ++ c).extraHeaders = (a ++ (b ++ c)).extraHeaders

ReqOption append is associative for the list-based fields.

theorem Network.HTTP.Req.option_queryParams_append_assoc {s : Scheme} (a b c : ReqOption s) : (a ++ b ++ c).queryParams = (a ++ (b ++ c)).queryParams

def Network.HTTP.Req.header {s : Scheme} (name : Types.HeaderName) (value : String) : ReqOption s

Add a custom header to the request.

Equations

• Network.HTTP.Req.header name value = { extraHeaders := [(name, value)] }

def Network.HTTP.Req.port {s : Scheme} (p : UInt16) : ReqOption s

Override the port.

Equations

• Network.HTTP.Req.port p = { portOverride := some p }

def Network.HTTP.Req.queryParam {s : Scheme} (key value : String) : ReqOption s

Add a query parameter.

Equations

• Network.HTTP.Req.queryParam key value = { queryParams := [(key, value)] }

def Network.HTTP.Req.queryFlag {s : Scheme} (key : String) : ReqOption s

Add a boolean query flag (parameter with no value).

Equations

• Network.HTTP.Req.queryFlag key = { queryParams := [(key, "")] }

def Network.HTTP.Req.responseTimeout {s : Scheme} (ms : Nat) : ReqOption s

Set the response timeout in milliseconds.

Equations

• Network.HTTP.Req.responseTimeout ms = { timeout := some ms }

def Network.HTTP.Req.basicAuth (user pass : String) : ReqOption Scheme.Https

Basic authentication. HTTPS-only enforced by the return type ReqOption .Https.

Using this with an http URL is a compile-time error: the type ReqOption .Https does not unify with ReqOption .Http.

$$\text{basicAuth} : \text{String} \to \text{String} \to \text{ReqOption .Https}$$

Equations

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

def Network.HTTP.Req.oAuth2Bearer (token : String) : ReqOption Scheme.Https

OAuth 2.0 bearer token. HTTPS-only. $$\text{oAuth2Bearer} : \text{String} \to \text{ReqOption .Https}$$

Equations

• Network.HTTP.Req.oAuth2Bearer token = { extraHeaders := [(Network.HTTP.Types.hAuthorization, toString "Bearer " ++ toString token)] }

def Network.HTTP.Req.oAuth2Token (token : String) : ReqOption Scheme.Https

OAuth 2.0 token (alternative form). HTTPS-only.

Equations

• Network.HTTP.Req.oAuth2Token token = { extraHeaders := [(Network.HTTP.Types.hAuthorization, toString "token " ++ toString token)] }

def Network.HTTP.Req.basicAuthUnsafe {s : Scheme} (user pass : String) : ReqOption s

Unsafe basic auth that works over any scheme. The caller is responsible for transport security.

Equations

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

structure Network.HTTP.Req.HttpConfig : Type

HTTP client configuration.

Controls redirect following, timeouts, and response validation. The redirectCount_le proof prevents unbounded redirect following.

$$\text{HttpConfig} = \{ \text{redirectCount} : \{n : \mathbb{N} \mid n \leq 100\},\; \text{timeout},\; \text{checkResponse} \}$$

• httpConfigRedirectCount : Nat

  Maximum number of redirects to follow.

• httpConfigTimeout : Nat

  Default response timeout in milliseconds. 0 = no timeout.

• httpConfigCheckResponse : Types.Status → Option String

  Custom response validation. Return some errorMsg to throw on non-2xx.

• redirectCount_le : self.httpConfigRedirectCount ≤ 100

  Redirect count is bounded (prevents unbounded recursion).

def Network.HTTP.Req.defaultHttpConfig : HttpConfig

Default HTTP config with sensible defaults.

Equations

• Network.HTTP.Req.defaultHttpConfig = { redirectCount_le := Network.HTTP.Req.defaultHttpConfig._proof_2 }

structure Network.HTTP.Req.Req (α : Type) : Type

The Req monad: IO with HTTP configuration via ReaderT pattern. $$\text{Req}\ \alpha = \text{HttpConfig} \to \text{IO}\ \alpha$$

• run : HttpConfig → IO α

  The underlying computation, a function from config to IO.

@[implicit_reducible]

instance Network.HTTP.Req.instFunctorReq : Functor Req

Equations

• Network.HTTP.Req.instFunctorReq = { map := fun {α β : Type} (f : α → β) (x : Network.HTTP.Req.Req α) => { run := fun (cfg : Network.HTTP.Req.HttpConfig) => f <$> x.run cfg } }

@[implicit_reducible]

instance Network.HTTP.Req.instPureReq : Pure Req

Equations

• Network.HTTP.Req.instPureReq = { pure := fun {α : Type} (a : α) => { run := fun (x : Network.HTTP.Req.HttpConfig) => pure a } }

@[implicit_reducible]

instance Network.HTTP.Req.instBindReq : Bind Req

Equations

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

@[implicit_reducible]

instance Network.HTTP.Req.instMonadReq : Monad Req

Equations

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

@[implicit_reducible]

instance Network.HTTP.Req.instMonadLiftIOReq : MonadLift IO Req

Equations

• Network.HTTP.Req.instMonadLiftIOReq = { monadLift := fun {α : Type} (action : IO α) => { run := fun (x : Network.HTTP.Req.HttpConfig) => action } }

class Network.HTTP.Req.MonadHttp (m : Type → Type) extends Monad m : Type 1

The MonadHttp typeclass. Any monad that can perform HTTP requests.

• map {α β : Type} : (α → β) → m α → m β
• mapConst {α β : Type} : α → m β → m α
• pure {α : Type} : α → m α
• seq {α β : Type} : m (α → β) → (Unit → m α) → m β
• seqLeft {α β : Type} : m α → (Unit → m β) → m α
• seqRight {α β : Type} : m α → (Unit → m β) → m β
• bind {α β : Type} : m α → (α → m β) → m β
• getHttpConfig : m HttpConfig

  Get the current HTTP configuration.

• handleHttpException {α : Type} : IO.Error → m α

  Handle an HTTP exception.

• liftIO {α : Type} : IO α → m α

  Lift an IO action into the monad.

@[implicit_reducible]

instance Network.HTTP.Req.instMonadHttpReq : MonadHttp Req

Equations

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

def Network.HTTP.Req.runReq {α : Type} (config : HttpConfig := defaultHttpConfig) (action : Req α) : IO α

Run a Req computation with the given configuration. $$\text{runReq} : \text{HttpConfig} \to \text{Req}\ \alpha \to \text{IO}\ \alpha$$

Equations

• Network.HTTP.Req.runReq config action = action.run config

def Network.HTTP.Req.req {methodTy bodyTy response : Type} {scheme : Scheme} [HttpMethod methodTy] [HttpBody bodyTy] [HttpResponse response] [HttpBodyAllowed (HttpMethod.allowsBody methodTy) (HttpBody.providesBody bodyTy)] (m : methodTy) (url : Url scheme) (b : bodyTy) (_responseHint : response) (options : ReqOption scheme := ∅) : Req response

Make a type-safe HTTP request.

This is the central function of the library. Type parameters enforce correctness at compile time:

• method must be an HttpMethod (GET, POST, etc.)
• body must be an HttpBody (NoReqBody, ReqBodyBs, etc.)
• response must be an HttpResponse (IgnoreResponse, BsResponse, etc.)
• HttpBodyAllowed ensures GET cannot carry a body
• scheme flows through Url and ReqOption, ensuring HTTPS-only auth

$$\text{req} : m \to \text{Url}\ s \to b \to r \to \text{ReqOption}\ s \to \text{Req}\ r$$

Equations

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

def Network.HTTP.Req.BsResponse.responseBody (r : BsResponse) : ByteArray

Get the response body from a BsResponse.

Equations

• r.responseBody = r.body

def Network.HTTP.Req.BsResponse.responseStatus (r : BsResponse) : Types.Status

Get the response status from a BsResponse.

Equations

• r.responseStatus = r.status

def Network.HTTP.Req.BsResponse.responseHeader (r : BsResponse) (name : Types.HeaderName) : Option String

Look up a header value in the response (case-insensitive).

Equations

• r.responseHeader name = Option.map Prod.snd (List.find? (fun (x : Network.HTTP.Types.Header) => match x with | (n, snd) => n == name) r.headers)

def Network.HTTP.Req.IgnoreResponse.responseStatus (r : IgnoreResponse) : Types.Status

Get the response status from an IgnoreResponse.

Equations

• r.responseStatus = r.status

def Network.HTTP.Req.IgnoreResponse.responseHeader (r : IgnoreResponse) (name : Types.HeaderName) : Option String

Look up a header value in an IgnoreResponse.

Equations

• r.responseHeader name = Option.map Prod.snd (List.find? (fun (x : Network.HTTP.Types.Header) => match x with | (n, snd) => n == name) r.headers)