From 106b39d2780a18fe4ae0e15ce0987edc0605feed Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Mon, 13 Apr 2026 17:47:58 -0300 Subject: [PATCH] fix: remove private from private section (#13398) This PR removes private from H1.lean --- src/Std/Internal/Http/Protocol/H1/Parser.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Std/Internal/Http/Protocol/H1/Parser.lean b/src/Std/Internal/Http/Protocol/H1/Parser.lean index 748cbfe3a5..decd1f9796 100644 --- a/src/Std/Internal/Http/Protocol/H1/Parser.lean +++ b/src/Std/Internal/Http/Protocol/H1/Parser.lean @@ -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" ||