fix: remove private from private section (#13398)

This PR removes private from H1.lean
This commit is contained in:
Sofia Rodrigues 2026-04-13 17:47:58 -03:00 committed by GitHub
parent cf53db3b13
commit 106b39d278
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -260,7 +260,7 @@ and returns the `RequestTarget` together with the raw major/minor version number
Both `parseRequestLine` and `parseRequestLineRawVersion` call this after consuming
the method token, keeping URI validation and version parsing in one place.
-/
private def parseRequestLineBody (limits : H1.Config) : Parser (RequestTarget × Nat × Nat) := do
def parseRequestLineBody (limits : H1.Config) : Parser (RequestTarget × Nat × Nat) := do
let rawUri ← parseURI limits <* sp
let uri ← match (Std.Http.URI.Parser.parseRequestTarget <* eof).run rawUri with
| .ok res => pure res
@ -446,7 +446,7 @@ Returns `true` if `name` (compared case-insensitively) is a field that MUST NOT
trailer sections per RFC 9112 §6.5. Forbidden fields are those required for message framing
(`content-length`, `transfer-encoding`), routing (`host`), or connection management (`connection`).
-/
private def isForbiddenTrailerField (name : String) : Bool :=
def isForbiddenTrailerField (name : String) : Bool :=
let n := name.toLower
n == "content-length" || n == "transfer-encoding" || n == "host" ||
n == "connection" || n == "expect" || n == "te" ||