lean4-htt/tests/elab/async.lean
Sofia Rodrigues 2e48cd293a
refactor: move Async and Http from Internal to Std (#13511)
This PR moves Async and Http from Internal to Std
2026-04-23 19:55:22 +00:00

47 lines
663 B
Text

import Std.Async
import Std.Internal.UV
import Std.Net.Addr
open Std.Async.UDP
open Std.Async
open Std.Net
def t : IO (Async Nat) := do
IO.println "a"
return do
IO.println "b"
return 2
-- Usage example of the ForIn instance
def loop : Async Nat := do
let mut res := 0
while res < 10 do
res := res + 1
discard t
pure res
/--
info: 10
-/
#guard_msgs in
#eval IO.println =<< ETask.block =<< loop.asTask
def loopExcept : Async Nat := do
let mut res := 0
while res < 10 do
throw (.userError "some error")
discard t
pure res
/--
error: some error
-/
#guard_msgs in
#eval IO.println =<< ETask.block =<< loopExcept.asTask