inductive PostgREST.Config.UriScheme : Type

URI scheme (HTTP or HTTPS).

• http : UriScheme
• https : UriScheme

@[implicit_reducible]

instance PostgREST.Config.instBEqUriScheme : BEq UriScheme

Equations

• PostgREST.Config.instBEqUriScheme = { beq := PostgREST.Config.instBEqUriScheme.beq }

def PostgREST.Config.instBEqUriScheme.beq : UriScheme → UriScheme → Bool

Equations

• PostgREST.Config.instBEqUriScheme.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance PostgREST.Config.instReprUriScheme : Repr UriScheme

Equations

• PostgREST.Config.instReprUriScheme = { reprPrec := PostgREST.Config.instReprUriScheme.repr }

def PostgREST.Config.instReprUriScheme.repr : UriScheme → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance PostgREST.Config.instToStringUriScheme : ToString UriScheme

Equations

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

def PostgREST.Config.UriScheme.defaultPort : UriScheme → Nat

The default port for a given scheme. $$\text{defaultPort}(\text{http}) = 80,\quad \text{defaultPort}(\text{https}) = 443$$

Equations

• PostgREST.Config.UriScheme.http.defaultPort = 80
• PostgREST.Config.UriScheme.https.defaultPort = 443

structure PostgREST.Config.ProxyUri : Type

A parsed proxy URI for OpenAPI server specification. $$\text{ProxyUri} = \{ \text{scheme},\; \text{host},\; \text{port} : \mathbb{N},\; \text{basePath} : \text{String} \}$$

• puScheme : UriScheme

  The URI scheme (http or https).

• puHost : String

  The hostname or IP address.

• puPort : Nat

  The port number.

• puBasePath : String

  The base path prefix (e.g., "/api/v1").

@[implicit_reducible]

instance PostgREST.Config.instBEqProxyUri : BEq ProxyUri

Equations

• PostgREST.Config.instBEqProxyUri = { beq := PostgREST.Config.instBEqProxyUri.beq }

def PostgREST.Config.instBEqProxyUri.beq : ProxyUri → ProxyUri → Bool

Equations

• One or more equations did not get rendered due to their size.
• PostgREST.Config.instBEqProxyUri.beq x✝¹ x✝ = false

def PostgREST.Config.instReprProxyUri.repr : ProxyUri → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance PostgREST.Config.instReprProxyUri : Repr ProxyUri

Equations

• PostgREST.Config.instReprProxyUri = { reprPrec := PostgREST.Config.instReprProxyUri.repr }

def PostgREST.Config.ProxyUri.toUri (p : ProxyUri) : String

Reconstruct the full URI string from parts. $$\text{toUri}(p) = \text{scheme}\texttt{://}\text{host}[:\text{port}]\text{basePath}$$

Equations

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

@[implicit_reducible]

instance PostgREST.Config.instToStringProxyUri : ToString ProxyUri

Equations

• PostgREST.Config.instToStringProxyUri = { toString := PostgREST.Config.ProxyUri.toUri }

def PostgREST.Config.ProxyUri.parse (uri : String) : Option ProxyUri

Parse a proxy URI string. $$\text{parse}(\texttt{https://api.example.com:8443/v1}) = \langle \text{https},\; \texttt{api.example.com},\; 8443,\; \texttt{/v1} \rangle$$

Returns none if the URI cannot be parsed. Handles:

• http:// and https:// schemes
• Optional port (defaults to 80 or 443)
• Optional path (defaults to "/")

Equations

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

def PostgREST.Config.openApiServerUrl (proxyUri : Option ProxyUri) (host : String) (port : Nat) : String

Generate the OpenAPI server URL from configuration. If a proxy URI is configured, use it. Otherwise, construct a URL from the server host and port.

Equations

• One or more equations did not get rendered due to their size.
• PostgREST.Config.openApiServerUrl (some proxy) host port = proxy.toUri