Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

HttpTypes – Core HTTP Types

Lean: Hale.HttpTypes | Haskell: http-types

Core HTTP/1.1 types: methods, status codes, headers, versions, and URI query parsing. Status codes carry a bounded proof (100 ≤ code ≤ 999).

Key Types

TypeDescription
StdMethodInductive of standard HTTP methods (GET, POST, HEAD, PUT, DELETE, etc.)
MethodStdMethod or custom String
StatusHTTP status with bounded 3-digit code (proof: 100 ≤ code ≤ 999)
HeaderNameCase-insensitive header name
HeaderHeaderName × ByteArray
HttpVersionMajor/minor pair with ordering
Query / QueryItemParsed query strings

API

FunctionSignature
parseQueryString → Query
renderQueryBool → Query → String
urlEncodeBool → ByteArray → ByteArray
urlDecodeBool → ByteArray → Option ByteArray

Files

  • Hale/HttpTypes/Network/HTTP/Types/Method.lean – StdMethod, Method
  • Hale/HttpTypes/Network/HTTP/Types/Status.lean – Status with bounded proof
  • Hale/HttpTypes/Network/HTTP/Types/Header.lean – Header types
  • Hale/HttpTypes/Network/HTTP/Types/Version.lean – HttpVersion
  • Hale/HttpTypes/Network/HTTP/Types/URI.lean – Query parsing and URL encoding