Task.spawn.{u} {α : Type u} (fn : Unit → α)
  (prio : Task.Priority := Task.Priority.default) : Task α
Task.spawn.{u} {α : Type u}
  (fn : Unit → α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  Task α

spawn fn : Task α 构造并立即启动一个新任务，以异步求值函数 fn () : α。

如果提供了 prio，它就是该任务的优先级。

Task.pure.{u} {α : Type u} (get : α) : Task α
Task.pure.{u} {α : Type u} (get : α) :
  Task α

Task.pure (a : α) 构造一个已经解析为值 a 的任务。

BaseIO.asTask {α : Type} (act : BaseIO α)
  (prio : Task.Priority := Task.Priority.default) : BaseIO (Task α)
BaseIO.asTask {α : Type} (act : BaseIO α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  BaseIO (Task α)

以优先级 prio 在单独的 Task 中运行 act。

运行所得的 BaseIO 操作会立即启动任务。对 Task 的纯访问不会影响非纯操作 act。

与通过 Task.spawn 创建的纯任务不同，即使任务的最后一个引用被丢弃，此函数创建的任务仍会运行。如果此时应终止该操作或让它对最后一个引用被丢弃作出其他响应，act 应通过 IO.checkCanceled 显式检查取消。

EIO.asTask {ε α : Type} (act : EIO ε α)
  (prio : Task.Priority := Task.Priority.default) :
  BaseIO (Task (Except ε α))
EIO.asTask {ε α : Type} (act : EIO ε α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  BaseIO (Task (Except ε α))

以优先级 prio 在单独的 Task 中运行 act。由于 EIO ε 操作可能抛出 ε 类型的异常，任务结果是 Except ε α。

运行所得的 IO 操作会立即启动任务。对 Task 的纯访问不会影响非纯操作 act。

与通过 Task.spawn 创建的纯任务不同，即使任务的最后一个引用被丢弃，此函数创建的任务仍会运行。如果此时应终止该操作或让它对最后一个引用被丢弃作出其他响应，act 应通过 IO.checkCanceled 显式检查取消。

IO.asTask {α : Type} (act : IO α)
  (prio : Task.Priority := Task.Priority.default) :
  BaseIO (Task (Except IO.Error α))
IO.asTask {α : Type} (act : IO α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  BaseIO (Task (Except IO.Error α))

以优先级 prio 在单独的 Task 中运行 act。由于 IO 操作可能抛出 IO.Error 类型的异常，任务结果是 Except IO.Error α。

运行所得的 BaseIO 操作会立即启动任务。对 Task 的纯访问不会影响非纯操作 act。由于 IO 操作可能抛出 IO.Error 类型的异常，任务结果是 Except IO.Error α。

与通过 Task.spawn 创建的纯任务不同，即使任务的最后一个引用被丢弃，此函数创建的任务仍会运行。如果此时应终止该操作或让它对最后一个引用被丢弃作出其他响应，act 应通过 IO.checkCanceled 显式检查取消。

Task.Priority : Type
Task.Priority : Type

任务优先级。

优先级较高的任务总是在优先级较低的任务之前调度。优先级高于 Task.Priority.max 的任务会在专用线程上调度。

Task.Priority.default : Task.Priority
Task.Priority.default : Task.Priority

所生成任务的默认优先级，也是最低优先级：0。

Task.Priority.max : Task.Priority
Task.Priority.max : Task.Priority

所生成任务的最高常规优先级：8。

以高于 Task.Priority.max 的优先级生成任务并非错误，但会为该任务生成专用工作线程。这由 Task.Priority.dedicated 表示。常规优先级任务会放入线程池，并按优先级顺序处理。

Task.Priority.dedicated : Task.Priority
Task.Priority.dedicated : Task.Priority

表示任务应在专用线程上调度。

任何高于 Task.Priority.max 的优先级都会使任务立即在专用线程上调度。这对长时间运行和/或受 I/O 限制的任务尤其有用，因为为减少上下文切换，Lean 默认分配的非专用工作线程不会超过核心数。

Std.Channel (α : Type) : Type
Std.Channel (α : Type) : Type

一种多生产者、多消费者的 FIFO 通道，既支持有界和无界缓冲，也提供异步 API。使用 Channel.sync 可切换到同步模式。

如果通道需要通过关闭来表示某种完成事件，请改用 Std.CloseableChannel。请注意，Std.CloseableChannel 在某些情况下需要错误处理，因此适用时通常更容易使用 Std.Channel。

Std.Channel.new {α : Type} (capacity : Option Nat := none) :
  BaseIO (Std.Channel α)
Std.Channel.new {α : Type}
  (capacity : Option Nat := none) :
  BaseIO (Std.Channel α)

创建新通道。若：

• capacity 为 none，通道无界（默认）

• capacity 为 some 0，发送方与接收方每次都必须会合

• capacity 为 some n 且 n > 0，通道使用大小为 n 的缓冲区，缓冲区填满后开始阻塞

Std.Channel.send {α : Type} (ch : Std.Channel α) (v : α) :
  BaseIO (Task Unit)
Std.Channel.send {α : Type}
  (ch : Std.Channel α) (v : α) :
  BaseIO (Task Unit)

通过通道发送一个值，并返回一个在传输完成后解析的任务。

Std.Channel.recv {α : Type} [Inhabited α] (ch : Std.Channel α) :
  BaseIO (Task α)
Std.Channel.recv {α : Type} [Inhabited α]
  (ch : Std.Channel α) : BaseIO (Task α)

从通道接收一个值，并返回一个在传输完成后解析的任务。请注意，如果通道在传输完成前关闭，该任务可能解析为 none。

Std.Channel.forAsync {α : Type} [Inhabited α] (f : α → BaseIO Unit)
  (ch : Std.Channel α) (prio : Task.Priority := Task.Priority.default) :
  BaseIO (Task Unit)
Std.Channel.forAsync {α : Type}
  [Inhabited α] (f : α → BaseIO Unit)
  (ch : Std.Channel α)
  (prio : Task.Priority :=
    Task.Priority.default) :
  BaseIO (Task Unit)

ch.forAsync f 对从 ch 接收的每条消息调用 f。

请注意，如果调用此函数两次，每条消息只会到达其中恰好一次调用。

Std.Channel.sync {α : Type} (ch : Std.Channel α) : Std.Channel.Sync α
Std.Channel.sync {α : Type}
  (ch : Std.Channel α) :
  Std.Channel.Sync α

此函数不执行任何操作，只是用于方便地公开通道的同步 API。

Std.Channel.Sync (α : Type) : Type
Std.Channel.Sync (α : Type) : Type

一种多生产者、多消费者的 FIFO 通道，既支持有界和无界缓冲，也提供同步 API。此类型只是以阻塞方式使用通道的便捷层，与原通道并无实际区别。

如果通道需要通过关闭来表示某种完成事件，请改用 Std.CloseableChannel.Sync。请注意，Std.CloseableChannel.Sync 在某些情况下需要错误处理，因此适用时通常更容易使用 Std.Channel.Sync。

Std.CloseableChannel (α : Type) : Type
Std.CloseableChannel (α : Type) : Type

一种多生产者、多消费者的 FIFO 通道，既支持有界和无界缓冲，也提供异步 API；使用 CloseableChannel.sync 可切换到同步模式。

此外，与 Std.Channel 不同，Std.CloseableChannel 可在需要时关闭。这在某些情况下会带来错误处理的需要，因此适用时通常更容易使用 Std.Channel。

Std.CloseableChannel.new {α : Type} (capacity : Option Nat := none) :
  BaseIO (Std.CloseableChannel α)
Std.CloseableChannel.new {α : Type}
  (capacity : Option Nat := none) :
  BaseIO (Std.CloseableChannel α)

创建新通道。若：

• capacity 为 none，通道无界（默认）

• capacity 为 some 0，发送方与接收方每次都必须会合

• capacity 为 some n 且 n > 0，通道使用大小为 n 的缓冲区，缓冲区填满后开始阻塞

Std.Mutex (α : Type) : Type
Std.Mutex (α : Type) : Type

保护 α 类型共享状态的互斥原语（锁）。

Mutex α 类型类似于 IO.Ref α，但并发访问由互斥锁保护，而不是通过原子指针操作和忙等待来保护。

Std.Mutex.new {α : Type} (a : α) : BaseIO (Std.Mutex α)
Std.Mutex.new {α : Type} (a : α) :
  BaseIO (Std.Mutex α)

创建一个新的互斥锁。

Std.Mutex.atomically {m : Type → Type} {α β : Type} [Monad m]
  [MonadLiftT BaseIO m] [MonadFinally m] (mutex : Std.Mutex α)
  (k : Std.AtomicT α m β) : m β
Std.Mutex.atomically {m : Type → Type}
  {α β : Type} [Monad m]
  [MonadLiftT BaseIO m] [MonadFinally m]
  (mutex : Std.Mutex α)
  (k : Std.AtomicT α m β) : m β

mutex.atomically k 在锁定互斥锁期间运行 k，使其可访问互斥锁的状态。

如果同一线程已持有底层 BaseMutex，再调用 mutex.atomically 属于未定义行为。如果代码无法避免这种情况，请考虑使用 RecursiveMutex。

Std.Mutex.atomicallyOnce {m : Type → Type} {α β : Type} [Monad m]
  [MonadLiftT BaseIO m] [MonadFinally m] (mutex : Std.Mutex α)
  (condvar : Std.Condvar) (pred : Std.AtomicT α m Bool)
  (k : Std.AtomicT α m β) : m β
Std.Mutex.atomicallyOnce {m : Type → Type}
  {α β : Type} [Monad m]
  [MonadLiftT BaseIO m] [MonadFinally m]
  (mutex : Std.Mutex α)
  (condvar : Std.Condvar)
  (pred : Std.AtomicT α m Bool)
  (k : Std.AtomicT α m β) : m β

mutex.atomicallyOnce condvar pred k 运行 k，并在 condvar 上等待，直到 pred 返回 true。k 和 pred 都可以访问互斥锁的状态。

如果同一线程已持有底层 BaseMutex，再调用 mutex.atomicallyOnce 属于未定义行为。如果代码无法避免这种情况，请考虑使用 RecursiveMutex。

Std.AtomicT (σ : Type) (m : Type → Type) (α : Type) : Type
Std.AtomicT (σ : Type) (m : Type → Type)
  (α : Type) : Type

AtomicT α m 是一种单子，可在 Mutex α 等互斥原语内部，以外层单子 m 原子地执行。 该操作可以通过 get 和 set 访问互斥锁的状态 α。

Std.Condvar : Type
Std.Condvar : Type

条件变量是一种与 BaseMutex 或 Mutex 配合使用的同步原语。

希望修改共享变量的线程必须：

1. 锁定 BaseMutex 或 Mutex

2. 操作共享变量

3. 完成后调用 Condvar.notifyOne 或 Condvar.notifyAll。请注意，这可以在解锁互斥锁之前或之后进行。

若使用 Mutex，等待 Condvar 的线程可以使用 Mutex.atomicallyOnce 等待条件成立。若使用 BaseMutex，则必须：

1. 锁定 BaseMutex。

2. 执行以下操作之一：

• 使用 Condvar.waitUntil 在条件变量上（可能反复）等待，直到条件成立。

• 按以下步骤手动实现等待：

  1. 检查条件

  2. 调用 Condvar.wait；它会释放 BaseMutex 并暂停执行，直到条件变量收到通知。

  3. 检查条件；如果尚未满足，则继续等待。

Std.Condvar.new : BaseIO Std.Condvar
Std.Condvar.new : BaseIO Std.Condvar

创建一个新的条件变量。

Std.Condvar.wait (condvar : Std.Condvar) (mutex : Std.BaseMutex) :
  BaseIO Unit
Std.Condvar.wait (condvar : Std.Condvar)
  (mutex : Std.BaseMutex) : BaseIO Unit

等待，直到另一线程调用 notifyOne 或 notifyAll。

Std.Condvar.notifyOne (condvar : Std.Condvar) : BaseIO Unit
Std.Condvar.notifyOne
  (condvar : Std.Condvar) : BaseIO Unit

唤醒一个正在执行 wait 的其他线程。

Std.Condvar.notifyAll (condvar : Std.Condvar) : BaseIO Unit
Std.Condvar.notifyAll
  (condvar : Std.Condvar) : BaseIO Unit

唤醒所有正在执行 wait 的其他线程。

Std.Condvar.waitUntil.{u_1} {m : Type → Type u_1} [Monad m]
  [MonadLiftT BaseIO m] (condvar : Std.Condvar) (mutex : Std.BaseMutex)
  (pred : m Bool) : m Unit
Std.Condvar.waitUntil.{u_1}
  {m : Type → Type u_1} [Monad m]
  [MonadLiftT BaseIO m]
  (condvar : Std.Condvar)
  (mutex : Std.BaseMutex)
  (pred : m Bool) : m Unit

在条件变量上等待，直到谓词为真。