def Network.Wai.Middleware.RequestLogger.formatJSON (req : Request) (status : HTTP.Types.Status) : String

Format a request as a JSON log line. Uses Lean's native Json type for structured output.

Equations

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

def Network.Wai.Middleware.RequestLogger.logJSON : IO Middleware

JSON logging middleware. $$\text{logJSON} : \text{IO Middleware}$$

Equations

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