fix: tests

src/Lean/Elab/Idbg.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Lean.Elab.Do.Basic
 meta import Lean.Parser.Do
-import Std.Internal.Async.TCP
+import Std.Async.TCP
 
 /-!
 # Interactive Debug Expression Evaluator (`idbg`)
@@ -22,7 +22,7 @@ and client (compiled program side) compute a deterministic port from the source
 -/
 
 open Lean Lean.Elab Lean.Elab.Term Lean.Meta
-open Std.Net Std.Internal.IO.Async
+open Std.Net Std.Async
 
 namespace Lean.Idbg
 

src/Std/Async.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+module
+
+prelude
+public import Std.Async.Basic
+public import Std.Async.ContextAsync
+public import Std.Async.Timer
+public import Std.Async.TCP
+public import Std.Async.UDP
+public import Std.Async.DNS
+public import Std.Async.Select
+public import Std.Async.Process
+public import Std.Async.System
+public import Std.Async.Signal
+public import Std.Async.IO

src/Std/Async/Basic.lean

@@ -12,8 +12,6 @@ public import Init.While
 public section
 
 namespace Std
-namespace Internal
-namespace IO
 namespace Async
 
 /-!
@@ -997,6 +995,4 @@ def background [Monad m] [MonadAsync t m] (action : m α) (prio := Task.Priority
   discard (async (t := t) (prio := prio) action)
 
 end Async
-end IO
-end Internal
 end Std

src/Std/Async/ContextAsync.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Std.Internal.UV
-public import Std.Internal.Async.Timer
+public import Std.Async.Timer
 public import Std.Sync.CancellationContext
 
 public section
@@ -18,8 +18,6 @@ cooperative cancellation support that must be explicitly checked for and cancell
 -/
 
 namespace Std
-namespace Internal
-namespace IO
 namespace Async
 
 /--
@@ -266,6 +264,4 @@ def Selector.cancelled : ContextAsync (Selector Unit) := do
   ContextAsync.doneSelector
 
 end Async
-end IO
-end Internal
 end Std

src/Std/Async/DNS.lean

@@ -8,14 +8,14 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV
-public import Std.Internal.Async.Basic
+public import Std.Async.Basic
 public import Init.Data.Function
 
 public section
 
+open Std.Internal
+
 namespace Std
-namespace Internal
-namespace IO
 namespace Async
 namespace DNS
 
@@ -59,6 +59,4 @@ def getNameInfo (host : @& SocketAddress) : Async NameInfo :=
 
 end DNS
 end Async
-end IO
-end Internal
 end Std

src/Std/Async/IO.lean

@@ -6,16 +6,15 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
 namespace Std
-namespace Internal
 namespace Async
 namespace IO
 
-open Std.Internal.IO.Async
+open Std.Async
 
 /-!
 This module provides buffered asynchronous I/O operations for efficient reading and writing.
@@ -50,5 +49,4 @@ class AsyncStream (α : Type) (β : outParam Type) where
 
 end IO
 end Async
-end Internal
 end Std

src/Std/Async/Process.lean

@@ -15,9 +15,9 @@ public section
 
 open Std Time
 open System
+open Std.Internal
 
 namespace Std
-namespace Internal
 namespace IO
 namespace Process
 
@@ -239,5 +239,4 @@ def availableMemory : IO UInt64 :=
 
 end Process
 end IO
-end Internal
 end Std

src/Std/Async/Select.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Random
-public import Std.Internal.Async.Basic
+public import Std.Async.Basic
 import Init.Data.ByteArray.Extra
 import Init.Data.Array.Lemmas
 import Init.Omega
@@ -21,8 +21,6 @@ The main entrypoint for users is `Selectable.one` and the various functions to p
 -/
 
 namespace Std
-namespace Internal
-namespace IO
 namespace Async
 
 /--
@@ -258,6 +256,4 @@ def Selectable.combine (selectables : Array (Selectable α)) : IO (Selector α)
   }
 
 end Async
-end IO
-end Internal
 end Std

src/Std/Async/Signal.lean

@@ -8,13 +8,11 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.Signal
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
 namespace Std
-namespace Internal
-namespace IO
 namespace Async
 
 /--

src/Std/Async/System.lean

@@ -19,10 +19,9 @@ manipulation.
 
 open Std Time
 open System
+open Std.Internal
 
 namespace Std
-namespace Internal
-namespace IO
 namespace Async
 namespace System
 
@@ -316,6 +315,4 @@ def getGroup (groupId : GroupId) : IO (Option GroupInfo) := do
 
 end System
 end Async
-end IO
-end Internal
 end Std

src/Std/Async/TCP.lean

@@ -8,13 +8,11 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.TCP
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
 namespace Std
-namespace Internal
-namespace IO
 namespace Async
 namespace TCP
 open Std.Net
@@ -258,6 +256,4 @@ end Client
 end Socket
 end TCP
 end Async
-end IO
-end Internal
 end Std

src/Std/Async/Timer.lean

@@ -8,14 +8,12 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.Timer
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
 
 namespace Std
-namespace Internal
-namespace IO
 namespace Async
 
 /--
@@ -168,6 +166,4 @@ def stop (i : Interval) : IO Unit :=
 end Interval
 
 end Async
-end IO
-end Internal
 end Std

src/Std/Async/UDP.lean

@@ -8,13 +8,11 @@ module
 prelude
 public import Std.Time
 public import Std.Internal.UV.UDP
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
 namespace Std
-namespace Internal
-namespace IO
 namespace Async
 namespace UDP
 
@@ -192,6 +190,4 @@ end Socket
 
 end UDP
 end Async
-end IO
-end Internal
 end Std

src/Std/Http.lean

@@ -6,8 +6,8 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Server
-public import Std.Internal.Http.Test.Helpers
+public import Std.Http.Server
+public import Std.Http.Test.Helpers
 
 public section
 
@@ -40,9 +40,9 @@ The main entry point is `Server.serve`, which starts an HTTP/1.1 server. Impleme
 `Expect: 100-continue` headers:
 
 ```lean
-import Std.Internal.Http
+import Std.Http
 
-open Std Internal IO Async
+open Std Async
 open Std Http Server
 
 structure MyHandler

src/Std/Http/Data.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Http.Data.Method
+public import Std.Http.Data.Version
+public import Std.Http.Data.Request
+public import Std.Http.Data.Response
+public import Std.Http.Data.Status
+public import Std.Http.Data.Chunk
+public import Std.Http.Data.Headers
+public import Std.Http.Data.URI
+public import Std.Http.Data.Body
+
+/-!
+# HTTP Data Types
+
+This module re-exports all HTTP data types including request/response structures,
+methods, status codes, chunks, and extension metadata.
+-/

src/Std/Http/Data/Body.lean

@@ -6,12 +6,12 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data.Body.Basic
-public import Std.Internal.Http.Data.Body.Length
-public import Std.Internal.Http.Data.Body.Any
-public import Std.Internal.Http.Data.Body.Stream
-public import Std.Internal.Http.Data.Body.Empty
-public import Std.Internal.Http.Data.Body.Full
+public import Std.Http.Data.Body.Basic
+public import Std.Http.Data.Body.Length
+public import Std.Http.Data.Body.Any
+public import Std.Http.Data.Body.Stream
+public import Std.Http.Data.Body.Empty
+public import Std.Http.Data.Body.Full
 
 public section
 

src/Std/Http/Data/Body/Any.lean

@@ -6,7 +6,7 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data.Body.Basic
+public import Std.Http.Data.Body.Basic
 
 public section
 
@@ -18,7 +18,7 @@ type that also implements `Http.Body`. Used as the default handler response body
 -/
 
 namespace Std.Http.Body
-open Std Internal IO Async
+open Std Async
 
 set_option linter.all true
 

src/Std/Http/Data/Body/Basic.lean

@@ -6,11 +6,11 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Async
-public import Std.Internal.Async.ContextAsync
-public import Std.Internal.Http.Data.Chunk
-public import Std.Internal.Http.Data.Headers
-public import Std.Internal.Http.Data.Body.Length
+public import Std.Async
+public import Std.Async.ContextAsync
+public import Std.Http.Data.Chunk
+public import Std.Http.Data.Headers
+public import Std.Http.Data.Body.Length
 
 public section
 
@@ -22,7 +22,7 @@ This module defines the `Body` typeclass for HTTP body streams, and shared conve
 -/
 
 namespace Std.Http
-open Std Internal IO Async
+open Std Async
 
 set_option linter.all true
 

src/Std/Http/Data/Body/Empty.lean

@@ -6,9 +6,9 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data.Request
-public import Std.Internal.Http.Data.Response
-public import Std.Internal.Http.Data.Body.Any
+public import Std.Http.Data.Request
+public import Std.Http.Data.Response
+public import Std.Http.Data.Body.Any
 
 public section
 
@@ -19,7 +19,7 @@ Represents an always-empty, already-closed body handle.
 -/
 
 namespace Std.Http.Body
-open Std Internal IO Async
+open Std Async
 
 set_option linter.all true
 
@@ -102,7 +102,7 @@ instance : Coe (Async (Response Empty)) (ContextAsync (Response Any)) where
 end Body
 
 namespace Request.Builder
-open Internal.IO.Async
+open Async
 
 /--
 Builds a request with no body.
@@ -113,7 +113,7 @@ def empty (builder : Builder) : Async (Request Body.Empty) :=
 end Request.Builder
 
 namespace Response.Builder
-open Internal.IO.Async
+open Async
 
 /--
 Builds a response with no body.

src/Std/Http/Data/Body/Full.lean

@@ -7,9 +7,9 @@ module
 
 prelude
 public import Std.Sync
-public import Std.Internal.Http.Data.Request
-public import Std.Internal.Http.Data.Response
-public import Std.Internal.Http.Data.Body.Any
+public import Std.Http.Data.Request
+public import Std.Http.Data.Response
+public import Std.Http.Data.Body.Any
 public import Init.Data.ByteArray
 
 public section
@@ -25,7 +25,7 @@ Closing the body discards any unconsumed data.
 -/
 
 namespace Std.Http.Body
-open Std Internal IO Async
+open Std Async
 
 set_option linter.all true
 
@@ -159,7 +159,7 @@ end Body
 
 namespace Request.Builder
 
-open Internal.IO.Async
+open Async
 
 /--
 Builds a request body from raw bytes without setting any headers.
@@ -200,7 +200,7 @@ def html (builder : Builder) (content : String) : Async (Request Body.Full) :=
 end Request.Builder
 
 namespace Response.Builder
-open Internal.IO.Async
+open Async
 
 /--
 Builds a response body from raw bytes without setting any headers.

src/Std/Http/Data/Body/Stream.lean

@@ -7,12 +7,12 @@ module
 
 prelude
 public import Std.Sync
-public import Std.Internal.Async
-public import Std.Internal.Http.Data.Request
-public import Std.Internal.Http.Data.Response
-public import Std.Internal.Http.Data.Chunk
-public import Std.Internal.Http.Data.Body.Basic
-public import Std.Internal.Http.Data.Body.Any
+public import Std.Async
+public import Std.Http.Data.Request
+public import Std.Http.Data.Response
+public import Std.Http.Data.Chunk
+public import Std.Http.Data.Body.Basic
+public import Std.Http.Data.Body.Any
 public import Init.Data.ByteArray
 
 public section
@@ -31,13 +31,13 @@ namespace Std.Http
 
 namespace Body
 
-open Std Internal IO Async
+open Std Async
 
 set_option linter.all true
 
 namespace Channel
 
-open Internal.IO.Async in
+open Async in
 private inductive Consumer where
   | normal (promise : IO.Promise (Option Chunk))
   | select (finished : Waiter (Option Chunk))
@@ -62,7 +62,7 @@ private structure Producer where
   -/
   done : IO.Promise Bool
 
-open Internal.IO.Async in
+open Async in
 private def resolveInterestWaiter (waiter : Waiter Bool) (x : Bool) : BaseIO Bool := do
   let lose := return false
   let win promise := do
@@ -84,7 +84,7 @@ private structure State where
   /--
   A waiter for `Stream.interestSelector`.
   -/
-  interestWaiter : Option (Internal.IO.Async.Waiter Bool)
+  interestWaiter : Option (Async.Waiter Bool)
 
   /--
   Whether the channel is closed.
@@ -299,7 +299,7 @@ def setKnownSize (stream : Stream) (size : Option Body.Length) : Async Unit :=
   stream.state.atomically do
     modify fun st => { st with knownSize := size }
 
-open Internal.IO.Async in
+open Async in
 
 /--
 Creates a selector that resolves when a producer is waiting (or the channel closes).
@@ -521,7 +521,7 @@ def hasInterest (stream : Stream) : Async Bool :=
     Channel.pruneFinishedWaiters
     Channel.hasInterest'
 
-open Internal.IO.Async in
+open Async in
 /--
 Creates a selector that resolves when consumer interest is present.
 Returns `true` when a consumer is waiting, `false` when the channel closes first.
@@ -634,7 +634,7 @@ end Body
 
 namespace Request.Builder
 
-open Internal.IO.Async
+open Async
 
 /--
 Builds a request with a streaming body generator.
@@ -649,7 +649,7 @@ def stream
 end Request.Builder
 
 namespace Response.Builder
-open Internal.IO.Async
+open Async
 
 /--
 Builds a response with a streaming body generator.

src/Std/Http/Data/Chunk.lean

@@ -6,9 +6,9 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Internal
-public import Std.Internal.Http.Data.Headers
-public meta import Std.Internal.Http.Internal.String
+public import Std.Http.Internal
+public import Std.Http.Data.Headers
+public meta import Std.Http.Internal.String
 
 public section
 

src/Std/Http/Data/Headers.lean

@@ -6,9 +6,9 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data.Headers.Basic
-public import Std.Internal.Http.Data.Headers.Name
-public import Std.Internal.Http.Data.Headers.Value
+public import Std.Http.Data.Headers.Basic
+public import Std.Http.Data.Headers.Name
+public import Std.Http.Data.Headers.Value
 
 public section
 

src/Std/Http/Data/Headers/Basic.lean

@@ -6,9 +6,9 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data.URI
-public import Std.Internal.Http.Data.Headers.Name
-public import Std.Internal.Http.Data.Headers.Value
+public import Std.Http.Data.URI
+public import Std.Http.Data.Headers.Name
+public import Std.Http.Data.Headers.Value
 public import Std.Internal.Parsec.Basic
 import Init.Data.String.Search
 

src/Std/Http/Data/Headers/Name.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.ToString
-public import Std.Internal.Http.Internal
+public import Std.Http.Internal
 import Init.Data.String.Search
 import Init.Data.String.Iter
 

src/Std/Http/Data/Headers/Value.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.ToString
-public import Std.Internal.Http.Internal
+public import Std.Http.Internal
 
 public section
 

src/Std/Http/Data/Method.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.ToString
-public import Std.Internal.Http.Internal
+public import Std.Http.Internal
 
 public section
 

src/Std/Http/Data/Request.lean

@@ -6,11 +6,11 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data.Extensions
-public import Std.Internal.Http.Data.Method
-public import Std.Internal.Http.Data.Version
-public import Std.Internal.Http.Data.Headers
-public import Std.Internal.Http.Data.URI
+public import Std.Http.Data.Extensions
+public import Std.Http.Data.Method
+public import Std.Http.Data.Version
+public import Std.Http.Data.Headers
+public import Std.Http.Data.URI
 
 public section
 

src/Std/Http/Data/Response.lean

@@ -6,10 +6,10 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data.Extensions
-public import Std.Internal.Http.Data.Status
-public import Std.Internal.Http.Data.Version
-public import Std.Internal.Http.Data.Headers
+public import Std.Http.Data.Extensions
+public import Std.Http.Data.Status
+public import Std.Http.Data.Version
+public import Std.Http.Data.Headers
 
 public section
 

src/Std/Http/Data/Status.lean

@@ -6,7 +6,7 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Internal
+public import Std.Http.Internal
 
 public section
 

src/Std/Http/Data/URI.lean

@@ -6,8 +6,8 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data.URI.Basic
-public import Std.Internal.Http.Data.URI.Parser
+public import Std.Http.Data.URI.Basic
+public import Std.Http.Data.URI.Parser
 
 public section
 

src/Std/Http/Data/URI/Basic.lean

@@ -8,8 +8,8 @@ module
 prelude
 import Init.Data.ToString
 public import Std.Net
-public import Std.Internal.Http.Internal
-public import Std.Internal.Http.Data.URI.Encoding
+public import Std.Http.Internal
+public import Std.Http.Data.URI.Encoding
 public import Init.Data.String.Search
 
 public section

src/Std/Http/Data/URI/Encoding.lean

@@ -13,7 +13,7 @@ import Init.Data.UInt.Lemmas
 import Init.Data.UInt.Bitwise
 import Init.Data.Array.Lemmas
 public import Init.Data.String.Basic
-public import Std.Internal.Http.Internal.Char
+public import Std.Http.Internal.Char
 
 public section
 

src/Std/Http/Data/URI/Parser.lean

@@ -10,8 +10,8 @@ import Init.While
 public import Init.Data.String.Basic
 public import Std.Internal.Parsec
 public import Std.Internal.Parsec.ByteArray
-public import Std.Internal.Http.Data.URI.Basic
-public import Std.Internal.Http.Data.URI.Config
+public import Std.Http.Data.URI.Basic
+public import Std.Http.Data.URI.Config
 import Init.Data.String.Search
 
 public section

src/Std/Http/Internal.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Http.Internal.Char
+public import Std.Http.Internal.ChunkedBuffer
+public import Std.Http.Internal.LowerCase
+public import Std.Http.Internal.IndexMultiMap
+public import Std.Http.Internal.Encode
+public import Std.Http.Internal.String
+public import Std.Http.Internal.Char
+
+/-!
+# HTTP Internal Utilities
+
+This module re-exports internal utilities used by the HTTP library including
+data structures, encoding functions, and buffer management.
+-/

src/Std/Http/Internal/Encode.lean

@@ -6,8 +6,8 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Internal.ChunkedBuffer
-public import Std.Internal.Http.Data.Version
+public import Std.Http.Internal.ChunkedBuffer
+public import Std.Http.Data.Version
 
 public section
 

src/Std/Http/Internal/String.lean

@@ -8,7 +8,7 @@ module
 prelude
 import Init.Grind
 public import Init.Data.String.TakeDrop
-public import Std.Internal.Http.Internal.Char
+public import Std.Http.Internal.Char
 
 public section
 

src/Std/Http/Protocol/H1.lean

@@ -8,14 +8,14 @@ module
 prelude
 public import Std.Time
 public import Init.Data.Array
-public import Std.Internal.Http.Data
-public import Std.Internal.Http.Internal
-public import Std.Internal.Http.Protocol.H1.Parser
-public import Std.Internal.Http.Protocol.H1.Config
-public import Std.Internal.Http.Protocol.H1.Message
-public import Std.Internal.Http.Protocol.H1.Reader
-public import Std.Internal.Http.Protocol.H1.Writer
-public import Std.Internal.Http.Protocol.H1.Event
+public import Std.Http.Data
+public import Std.Http.Internal
+public import Std.Http.Protocol.H1.Parser
+public import Std.Http.Protocol.H1.Config
+public import Std.Http.Protocol.H1.Message
+public import Std.Http.Protocol.H1.Reader
+public import Std.Http.Protocol.H1.Writer
+public import Std.Http.Protocol.H1.Event
 
 public section
 

src/Std/Http/Protocol/H1/Config.lean

@@ -6,8 +6,8 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Data
-public import Std.Internal.Http.Internal
+public import Std.Http.Data
+public import Std.Http.Internal
 
 public section
 

src/Std/Http/Protocol/H1/Error.lean

@@ -7,11 +7,11 @@ module
 
 prelude
 public import Std.Time
-public import Std.Internal.Http.Data
-public import Std.Internal.Http.Internal
-public import Std.Internal.Http.Protocol.H1.Parser
-public import Std.Internal.Http.Protocol.H1.Config
-public import Std.Internal.Http.Protocol.H1.Message
+public import Std.Http.Data
+public import Std.Http.Internal
+public import Std.Http.Protocol.H1.Parser
+public import Std.Http.Protocol.H1.Config
+public import Std.Http.Protocol.H1.Message
 
 public section
 

src/Std/Http/Protocol/H1/Event.lean

@@ -7,12 +7,12 @@ module
 
 prelude
 public import Std.Time
-public import Std.Internal.Http.Data
-public import Std.Internal.Http.Internal
-public import Std.Internal.Http.Protocol.H1.Parser
-public import Std.Internal.Http.Protocol.H1.Config
-public import Std.Internal.Http.Protocol.H1.Message
-public import Std.Internal.Http.Protocol.H1.Error
+public import Std.Http.Data
+public import Std.Http.Internal
+public import Std.Http.Protocol.H1.Parser
+public import Std.Http.Protocol.H1.Config
+public import Std.Http.Protocol.H1.Message
+public import Std.Http.Protocol.H1.Error
 
 public section
 

src/Std/Http/Protocol/H1/Message.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.Array
-public import Std.Internal.Http.Data
+public import Std.Http.Data
 
 public section
 

src/Std/Http/Protocol/H1/Parser.lean

@@ -7,9 +7,9 @@ module
 
 prelude
 public import Std.Internal.Parsec
-public import Std.Internal.Http.Data
+public import Std.Http.Data
 public import Std.Internal.Parsec.ByteArray
-public import Std.Internal.Http.Protocol.H1.Config
+public import Std.Http.Protocol.H1.Config
 
 /-!
 This module defines parsers for HTTP/1.1 request and response lines, headers, and body framing. The

src/Std/Http/Protocol/H1/Reader.lean

@@ -7,12 +7,12 @@ module
 
 prelude
 public import Std.Time
-public import Std.Internal.Http.Data
-public import Std.Internal.Http.Internal
-public import Std.Internal.Http.Protocol.H1.Parser
-public import Std.Internal.Http.Protocol.H1.Config
-public import Std.Internal.Http.Protocol.H1.Message
-public import Std.Internal.Http.Protocol.H1.Error
+public import Std.Http.Data
+public import Std.Http.Internal
+public import Std.Http.Protocol.H1.Parser
+public import Std.Http.Protocol.H1.Config
+public import Std.Http.Protocol.H1.Message
+public import Std.Http.Protocol.H1.Error
 
 public section
 

src/Std/Http/Protocol/H1/Writer.lean

@@ -7,12 +7,12 @@ module
 
 prelude
 public import Std.Time
-public import Std.Internal.Http.Data
-public import Std.Internal.Http.Internal
-public import Std.Internal.Http.Protocol.H1.Parser
-public import Std.Internal.Http.Protocol.H1.Config
-public import Std.Internal.Http.Protocol.H1.Message
-public import Std.Internal.Http.Protocol.H1.Error
+public import Std.Http.Data
+public import Std.Http.Internal
+public import Std.Http.Protocol.H1.Parser
+public import Std.Http.Protocol.H1.Config
+public import Std.Http.Protocol.H1.Message
+public import Std.Http.Protocol.H1.Error
 
 public section
 

src/Std/Http/Server.lean

@@ -6,13 +6,13 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Async
-public import Std.Internal.Async.TCP
+public import Std.Async
+public import Std.Async.TCP
 public import Std.Sync.CancellationToken
 public import Std.Sync.Semaphore
-public import Std.Internal.Http.Server.Config
-public import Std.Internal.Http.Server.Handler
-public import Std.Internal.Http.Server.Connection
+public import Std.Http.Server.Config
+public import Std.Http.Server.Handler
+public import Std.Http.Server.Connection
 
 public section
 
@@ -30,7 +30,7 @@ promise once all connections have closed.
 -/
 
 namespace Std.Http
-open Std.Internal.IO.Async TCP
+open Std.Async TCP
 
 set_option linter.all true
 

src/Std/Http/Server/Config.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Std.Time
-public import Std.Internal.Http.Protocol.H1
+public import Std.Http.Protocol.H1
 
 public section
 

src/Std/Http/Server/Connection.lean

@@ -6,12 +6,12 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Async.TCP
-public import Std.Internal.Async.ContextAsync
-public import Std.Internal.Http.Transport
-public import Std.Internal.Http.Protocol.H1
-public import Std.Internal.Http.Server.Config
-public import Std.Internal.Http.Server.Handler
+public import Std.Async.TCP
+public import Std.Async.ContextAsync
+public import Std.Http.Transport
+public import Std.Http.Protocol.H1
+public import Std.Http.Server.Config
+public import Std.Http.Server.Handler
 
 public section
 
@@ -19,7 +19,7 @@ namespace Std
 namespace Http
 namespace Server
 
-open Std Internal IO Async TCP Protocol
+open Std Async TCP Protocol
 open Time
 
 /-!
@@ -73,7 +73,7 @@ private inductive Recv (β : Type)
   | bytes (x : Option ByteArray)
   | responseBody (x : Option Chunk)
   | bodyInterest (x : Bool)
-  | response (x : (Except Error (Response β)))
+  | response (x : (Except IO.Error (Response β)))
   | timeout
   | shutdown
   | close
@@ -85,7 +85,7 @@ Each `Option` field is `none` when that source is not currently active.
 private structure PollSources (α β : Type) where
   socket : Option α
   expect : Option Nat
-  response : Option (Std.Channel (Except Error (Response β)))
+  response : Option (Std.Channel (Except IO.Error (Response β)))
   responseBody : Option β
   requestBody : Option Body.Stream
   timeout : Millisecond.Offset
@@ -214,7 +214,7 @@ private structure ConnectionState (β : Type) where
   keepAliveTimeout : Option Millisecond.Offset
   currentTimeout : Millisecond.Offset
   headerTimeout : Option Timestamp
-  response : Std.Channel (Except Error (Response β))
+  response : Std.Channel (Except IO.Error (Response β))
   respStream : Option β
   requiresData : Bool
   expectData : Option Nat

src/Std/Http/Server/Handler.lean

@@ -6,15 +6,15 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Async
-public import Std.Internal.Http.Data
-public import Std.Internal.Async.ContextAsync
+public import Std.Async
+public import Std.Http.Data
+public import Std.Async.ContextAsync
 
 public section
 
 namespace Std.Http.Server
 
-open Std.Internal.IO.Async
+open Std.Async
 
 set_option linter.all true
 

src/Std/Http/Test/Helpers.lean

@@ -6,14 +6,14 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Server
-public import Std.Internal.Async
-public import Std.Internal.Async.Timer
+public import Std.Http.Server
+public import Std.Async
+public import Std.Async.Timer
 import Init.Data.String.Legacy
 
 public section
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http
 
 namespace Std.Http.Internal.Test

src/Std/Http/Transport.lean

@@ -6,7 +6,7 @@ Authors: Sofia Rodrigues
 module
 
 prelude
-public import Std.Internal.Http.Protocol.H1
+public import Std.Http.Protocol.H1
 
 public section
 
@@ -18,7 +18,7 @@ that can be used with an HTTP connection.
 -/
 
 namespace Std.Http
-open Std Internal IO Async TCP
+open Std Async TCP
 
 set_option linter.all true
 
@@ -56,7 +56,7 @@ instance : Transport Socket.Client where
 
 namespace Internal
 
-open Internal.IO.Async in
+open Async in
 
 /--
 Shared state for a bidirectional mock connection.

src/Std/Internal.lean

@@ -6,8 +6,8 @@ Authors: Henrik Böving
 module
 
 prelude
-public import Std.Internal.Async
-public import Std.Internal.Http
+public import Std.Async
+public import Std.Http
 public import Std.Internal.Parsec
 public import Std.Internal.UV
 

src/Std/Internal/Async.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-module
-
-prelude
-public import Std.Internal.Async.Basic
-public import Std.Internal.Async.ContextAsync
-public import Std.Internal.Async.Timer
-public import Std.Internal.Async.TCP
-public import Std.Internal.Async.UDP
-public import Std.Internal.Async.DNS
-public import Std.Internal.Async.Select
-public import Std.Internal.Async.Process
-public import Std.Internal.Async.System
-public import Std.Internal.Async.Signal
-public import Std.Internal.Async.IO

src/Std/Internal/Http/Data.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Internal.Http.Data.Method
-public import Std.Internal.Http.Data.Version
-public import Std.Internal.Http.Data.Request
-public import Std.Internal.Http.Data.Response
-public import Std.Internal.Http.Data.Status
-public import Std.Internal.Http.Data.Chunk
-public import Std.Internal.Http.Data.Headers
-public import Std.Internal.Http.Data.URI
-public import Std.Internal.Http.Data.Body
-
-/-!
-# HTTP Data Types
-
-This module re-exports all HTTP data types including request/response structures,
-methods, status codes, chunks, and extension metadata.
--/

src/Std/Internal/Http/Internal.lean

@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sofia Rodrigues
--/
-module
-
-prelude
-public import Std.Internal.Http.Internal.Char
-public import Std.Internal.Http.Internal.ChunkedBuffer
-public import Std.Internal.Http.Internal.LowerCase
-public import Std.Internal.Http.Internal.IndexMultiMap
-public import Std.Internal.Http.Internal.Encode
-public import Std.Internal.Http.Internal.String
-public import Std.Internal.Http.Internal.Char
-
-/-!
-# HTTP Internal Utilities
-
-This module re-exports internal utilities used by the HTTP library including
-data structures, encoding functions, and buffer management.
--/

src/Std/Sync/Broadcast.lean

@@ -10,14 +10,14 @@ public import Std.Data
 public import Init.Data.Queue
 public import Init.Data.Vector
 public import Std.Sync.Mutex
-public import Std.Internal.Async.IO
+public import Std.Async.IO
 
 public section
 
 namespace Std
 
-open Std.Internal.Async.IO
-open Std.Internal.IO.Async
+open Std.Async.IO
+open Std.Async
 
 /-!
 The `Std.Sync.Broadcast` module implements a broadcasting primitive for sending values
@@ -60,7 +60,7 @@ instance instMonadLiftBroadcastIO : MonadLift (EIO Broadcast.Error) IO where
 
 private structure Broadcast.Consumer (α : Type) where
   promise : IO.Promise Bool
-  waiter : Option (Internal.IO.Async.Waiter (Option α))
+  waiter : Option (Async.Waiter (Option α))
 
 private def Broadcast.Consumer.resolve (c : Broadcast.Consumer α) (b : Bool) : BaseIO Unit :=
   c.promise.resolve b
@@ -403,7 +403,7 @@ private def recvReady'
     let slotVal ← slot.get
     return slotVal.pos = next
 
-open Internal.IO.Async in
+open Async in
 private partial def recvSelector (ch : Bounded.Receiver α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -537,7 +537,7 @@ the next available message. This will block until a message is available.
 def recv [Inhabited α] (ch : Broadcast.Receiver α) : BaseIO (Task (Option α)) := do
   Std.Bounded.Receiver.recv ch.inner
 
-open Internal.IO.Async in
+open Async in
 
 /--
 Creates a `Selector` that resolves once the broadcast channel `ch` has data available and provides that data.
@@ -567,7 +567,7 @@ instance [Inhabited α] : AsyncStream (Broadcast.Receiver α) (Option α) where
   stop channel := channel.unsubscribe
 
 instance [Inhabited α] : AsyncRead (Broadcast.Receiver α) (Option α) where
-  read receiver := Internal.IO.Async.Async.ofIOTask receiver.recv
+  read receiver := Async.ofIOTask receiver.recv
 
 instance [Inhabited α] : AsyncWrite (Broadcast α) α where
   write receiver x := do

src/Std/Sync/CancellationContext.lean

@@ -17,7 +17,7 @@ automatically cancels all child contexts.
 -/
 
 namespace Std
-open Std.Internal.IO.Async
+open Std.Async
 
 structure CancellationContext.State where
   /--

src/Std/Sync/CancellationToken.lean

@@ -9,7 +9,7 @@ prelude
 public import Std.Data
 public import Init.Data.Queue
 public import Std.Sync.Mutex
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 public import Init.Data.ToString.Macro
 
 public section
@@ -22,7 +22,7 @@ that a cancellation has occurred.
 -/
 
 namespace Std
-open Std.Internal.IO.Async
+open Std.Async
 
 /--
 Reasons for cancellation.

src/Std/Sync/Channel.lean

@@ -8,15 +8,15 @@ module
 prelude
 public import Init.Data.Queue
 public import Std.Sync.Mutex
-public import Std.Internal.Async.IO
+public import Std.Async.IO
 import Init.Data.Vector.Basic
 import Init.Data.Option.BasicAux
 import Init.Omega
 
 public section
 
-open Std.Internal.Async.IO
-open Std.Internal.IO.Async
+open Std.Async.IO
+open Std.Async
 
 /-!
 This module contains the implementation of `Std.Channel`. `Std.Channel` is a multi-producer
@@ -53,7 +53,7 @@ instance : ToString Error where
 instance : MonadLift (EIO Error) IO where
   monadLift x := EIO.toIO (.userError <| toString ·) x
 
-open Internal.IO.Async in
+open Async in
 private inductive Consumer (α : Type) where
   | normal (promise : IO.Promise (Option α))
   | select (finished : Waiter (Option α))
@@ -174,7 +174,7 @@ private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
   let st ← get
   return !st.values.isEmpty || st.closed
 
-open Internal.IO.Async in
+open Async in
 private def recvSelector (ch : Unbounded α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -324,7 +324,7 @@ private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
   let st ← get
   return !st.producers.isEmpty || st.closed
 
-open Internal.IO.Async in
+open Async in
 private def recvSelector (ch : Zero α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -358,7 +358,7 @@ private def recvSelector (ch : Zero α) : Selector (Option α) where
 
 end Zero
 
-open Internal.IO.Async in
+open Async in
 private structure Bounded.Consumer (α : Type) where
   promise : IO.Promise Bool
   waiter : Option (Waiter (Option α))
@@ -560,7 +560,7 @@ private def recvReady' [Monad m] [MonadLiftT (ST IO.RealWorld) m] :
   let st ← get
   return st.bufCount != 0 || st.closed
 
-open Internal.IO.Async in
+open Async in
 private partial def recvSelector (ch : Bounded α) : Selector (Option α) where
   tryFn := do
     ch.state.atomically do
@@ -734,7 +734,7 @@ def recv (ch : CloseableChannel α) : BaseIO (Task (Option α)) :=
   | .zero ch => CloseableChannel.Zero.recv ch
   | .bounded ch => CloseableChannel.Bounded.recv ch
 
-open Internal.IO.Async in
+open Async in
 /--
 Creates a `Selector` that resolves once `ch` has data available and provides that data.
 In particular if `ch` is closed while waiting on this `Selector` and no data is available already
@@ -761,7 +761,7 @@ instance [Inhabited α] : AsyncStream (CloseableChannel α) (Option α) where
   next channel := channel.recvSelector
 
 instance [Inhabited α] : AsyncRead (CloseableChannel α) (Option α) where
-  read receiver := Internal.IO.Async.Async.ofIOTask receiver.recv
+  read receiver := Async.ofIOTask receiver.recv
 
 instance [Inhabited α] : AsyncWrite (CloseableChannel α) α where
   write receiver x := do
@@ -879,7 +879,7 @@ def recv [Inhabited α] (ch : Channel α) : BaseIO (Task α) := do
       | some val => return .pure val
       | none => unreachable!
 
-open Internal.IO.Async in
+open Async in
 /--
 Creates a `Selector` that resolves once `ch` has data available and provides that data.
 -/
@@ -911,7 +911,7 @@ instance [Inhabited α] : AsyncStream (Channel α) α where
   next channel := channel.recvSelector
 
 instance [Inhabited α] : AsyncRead (Channel α) α where
-  read receiver := Internal.IO.Async.Async.ofIOTask receiver.recv
+  read receiver := Async.ofIOTask receiver.recv
 
 instance [Inhabited α] : AsyncWrite (Channel α) α where
   write receiver x := do

src/Std/Sync/Notify.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Data.Queue
 public import Std.Sync.Mutex
-public import Std.Internal.Async.Select
+public import Std.Async.Select
 
 public section
 
@@ -24,7 +24,7 @@ will be woken up per notification.
 -/
 
 namespace Std
-open Std.Internal.IO.Async
+open Std.Async
 
 inductive Notify.Consumer (α : Type) where
   | normal (promise : IO.Promise α)

src/Std/Sync/StreamMap.lean

@@ -8,12 +8,12 @@ module
 prelude
 public import Std.Data
 public import Init.Data.Queue
-public import Std.Internal.Async.IO
+public import Std.Async.IO
 
 public section
 
-open Std.Internal.Async.IO
-open Std.Internal.IO.Async
+open Std.Async.IO
+open Std.Async
 
 /-!
 This module provides `StreamMap`, a container that maps keys to async streams.

tests/elab/async.lean

@@ -1,9 +1,9 @@
-import Std.Internal.Async
+import Std.Async
 import Std.Internal.UV
 import Std.Net.Addr
 
-open Std.Internal.IO.Async.UDP
-open Std.Internal.IO.Async
+open Std.Async.UDP
+open Std.Async
 open Std.Net
 
 def t : IO (Async Nat) := do

tests/elab/async_base_functions.lean

@@ -1,9 +1,9 @@
-import Std.Internal.Async
+import Std.Async
 import Std.Sync.Mutex
 
 open Std
 
-open Std.Internal.IO.Async
+open Std.Async
 
 def wait (ms : UInt32) (ref : Std.Mutex Nat) (val : Nat) : Async Unit := do
   ref.atomically (·.modify (· * val))

tests/elab/async_cancellation.lean

@@ -1,7 +1,7 @@
-import Std.Internal.Async
+import Std.Async
 import Std.Sync
 
-open Std.Internal.IO Async
+open Std Async
 
 def cancellableSelector [Monad m] [MonadLift IO m] [MonadAsync AsyncTask m] (fn : Std.CancellationToken → m α) : m (Selector (Except IO.Error α)) := do
   let signal ← Std.CancellationToken.new

tests/elab/async_cancellation_reasons.lean

@@ -1,7 +1,7 @@
-import Std.Internal.Async
+import Std.Async
 import Std.Sync
 
-open Std.Internal.IO Async
+open Std Async
 
 -- Test basic cancellation with default reason
 def testBasicCancellationWithReason : Async Unit := do

tests/elab/async_dns.lean

@@ -1,8 +1,8 @@
-import Std.Internal.Async
+import Std.Async
 import Std.Internal.UV
 import Std.Net.Addr
 
-open Std.Internal.IO Async
+open Std.Async
 open Std.Net
 
 open Std.Net

tests/elab/async_http_body.lean

@@ -1,6 +1,6 @@
-import Std.Internal.Http.Data.Body
+import Std.Http.Data.Body
 
-open Std.Internal.IO Async
+open Std.Async
 open Std.Http
 open Std.Http.Body
 

tests/elab/async_http_body_framing.lean

@@ -1,6 +1,6 @@
-import Std.Internal.Http.Test.Helpers
+import Std.Http.Test.Helpers
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 -- RFC 9112 §6: Transfer-Encoding and Content-Length framing

tests/elab/async_http_dispatch.lean

@@ -1,6 +1,6 @@
-import Std.Internal.Http.Test.Helpers
+import Std.Http.Test.Helpers
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 -- Basic method dispatch and streaming responses

tests/elab/async_http_encode.lean

@@ -1,6 +1,6 @@
-import Std.Internal.Http.Data.Chunk
-import Std.Internal.Http.Data.Request
-import Std.Internal.Http.Data.Response
+import Std.Http.Data.Chunk
+import Std.Http.Data.Request
+import Std.Http.Data.Response
 
 open Std.Http
 open Std.Http.Internal

tests/elab/async_http_expect.lean

@@ -1,6 +1,6 @@
-import Std.Internal.Http.Test.Helpers
+import Std.Http.Test.Helpers
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 -- Handlers for Expect: 100-continue testing

tests/elab/async_http_fuzz.lean

@@ -1,8 +1,8 @@
-import Std.Internal.Http
-import Std.Internal.Async
-import Std.Internal.Async.Timer
+import Std.Http
+import Std.Async
+import Std.Async.Timer
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 

tests/elab/async_http_fuzz_limits.lean

@@ -1,7 +1,7 @@
-import Std.Internal.Http
-import Std.Internal.Async
+import Std.Http
+import Std.Async
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 /-!

tests/elab/async_http_fuzz_random.lean

@@ -1,7 +1,7 @@
-import Std.Internal.Http
-import Std.Internal.Async
+import Std.Http
+import Std.Async
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 /-!

tests/elab/async_http_h1_incremental.lean

@@ -1,4 +1,4 @@
-import Std.Internal.Http
+import Std.Http
 
 open Std Http
 open Std.Http.Protocol.H1

tests/elab/async_http_h1_parser_fuzz.lean

@@ -1,5 +1,5 @@
-import Std.Internal.Http
-import Std.Internal.Http.Protocol.H1.Parser
+import Std.Http
+import Std.Http.Protocol.H1.Parser
 
 open Std Internal Parsec ByteArray
 open Std.Http.Protocol.H1

tests/elab/async_http_h1_rfc_compliance.lean

@@ -1,4 +1,4 @@
-import Std.Internal.Http
+import Std.Http
 
 open Std Http
 open Std.Http.Internal.Test

tests/elab/async_http_hang_regressions.lean

@@ -1,8 +1,8 @@
-import Std.Internal.Http
-import Std.Internal.Async
-import Std.Internal.Async.Timer
+import Std.Http
+import Std.Async
+import Std.Async.Timer
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 def runWithTimeout {α : Type} (name : String) (timeoutMs : Nat := 2000) (action : IO α) : IO α := do

tests/elab/async_http_headers.lean

@@ -1,5 +1,5 @@
-import Std.Internal.Http.Data.Headers
-import Std.Internal.Http.Protocol.H1
+import Std.Http.Data.Headers
+import Std.Http.Protocol.H1
 
 open Std.Http
 open Std.Http.Header

tests/elab/async_http_keepalive.lean

@@ -1,6 +1,6 @@
-import Std.Internal.Http.Test.Helpers
+import Std.Http.Test.Helpers
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 -- Helper: run pipelined raw request string, closing the client after send.

tests/elab/async_http_request_headers.lean

@@ -1,6 +1,6 @@
-import Std.Internal.Http.Test.Helpers
+import Std.Http.Test.Helpers
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 -- Shared fixtures

tests/elab/async_http_request_line.lean

@@ -1,6 +1,6 @@
-import Std.Internal.Http.Test.Helpers
+import Std.Http.Test.Helpers
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 -- Shared fixtures

tests/elab/async_http_response_framing.lean

@@ -1,6 +1,6 @@
-import Std.Internal.Http.Test.Helpers
+import Std.Http.Test.Helpers
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 
 -- Shared fixtures

tests/elab/async_http_string_quoting.lean

@@ -1,5 +1,5 @@
-import Std.Internal.Http.Internal.String
-import Std.Internal.Http.Internal.Char
+import Std.Http.Internal.String
+import Std.Http.Internal.Char
 
 open Std.Http.Internal
 

tests/elab/async_http_trailers.lean

@@ -1,7 +1,7 @@
-import Std.Internal.Http
-import Std.Internal.Async
+import Std.Http
+import Std.Async
 
-open Std.Internal.IO Async
+open Std.Async
 open Std Http Internal Test
 open Std.Http.Internal
 

tests/elab/async_http_uri.lean

@@ -3,8 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sofia Rodrigues
 -/
-import Std.Internal.Http.Data.URI
-import Std.Internal.Http.Data.URI.Encoding
+import Std.Http.Data.URI
+import Std.Http.Data.URI.Encoding
 
 open Std.Http
 open Std.Http.URI

tests/elab/async_select_channel.lean

@@ -1,6 +1,6 @@
 import Std.Sync.Channel
 
-open Std Internal IO Async
+open Std Async
 
 namespace A
 

tests/elab/async_select_gate.lean

@@ -1,7 +1,7 @@
-import Std.Internal.Async.Select
+import Std.Async.Select
 import Std.Sync.Channel
 
-open Std Internal IO Async
+open Std Async
 
 /-!
 Tests for the `gate` in `Selectable.one`.

tests/elab/async_select_socket.lean

@@ -1,10 +1,10 @@
-import Std.Internal.Async.Timer
-import Std.Internal.Async.TCP
-import Std.Internal.Async.UDP
+import Std.Async.Timer
+import Std.Async.TCP
+import Std.Async.UDP
 
 #exit -- TODO: remove `#exit` after nondet issue is resolved.
 
-open Std Internal IO Async
+open Std Async
 
 namespace TCP
 

tests/elab/async_select_timer.lean

@@ -1,6 +1,6 @@
-import Std.Internal.Async.Timer
+import Std.Async.Timer
 
-open Std Internal IO Async
+open Std Async
 
 def test1 : Async Nat := do
   let s1 ← Sleep.mk 1000

tests/elab/async_streammap.lean

@@ -1,7 +1,7 @@
-import Std.Internal.Async
+import Std.Async
 import Std.Sync
 
-open Std.Internal.IO Async
+open Std.Async
 
 -- Test basic message reception from multiple channels
 def testSimpleMessages : Async Unit := do

tests/elab/async_surface_sleep.lean

@@ -1,11 +1,11 @@
-import Std.Internal.Async.Timer
+import Std.Async.Timer
 
 /-
 these tests are just some preliminary ones as `async_sleep.lean` already contains extensive tests
 for the entire timer state machine and `Async.Timer` is merely a light wrapper around it.
 -/
 
-open Std.Internal.IO.Async
+open Std.Async
 
 def BASE_DURATION : Std.Time.Millisecond.Offset := 10