GreenThread

def Control.Concurrent.Scheduler.PosNat : Type

A positive natural number, reused from Control.Concurrent.

Equations

• Control.Concurrent.Scheduler.PosNat = { n : Nat // n > 0 }

instance Control.Concurrent.Scheduler.instNonemptyPosNat : Nonempty PosNat

@[implicit_reducible]

instance Control.Concurrent.Scheduler.instBEqPosNat : BEq PosNat

Equations

• Control.Concurrent.Scheduler.instBEqPosNat = { beq := fun (a b : Control.Concurrent.Scheduler.PosNat) => a.val == b.val }

@[implicit_reducible]

instance Control.Concurrent.Scheduler.instToStringPosNat : ToString PosNat

Equations

• Control.Concurrent.Scheduler.instToStringPosNat = { toString := fun (p : Control.Concurrent.Scheduler.PosNat) => toString p.val }

structure Control.Concurrent.Scheduler.GreenThread : Type

A lightweight green thread queued for execution.

• id — unique identifier (monotonic, $\ge 1$).
• action — the IO Unit closure to run.
• token — cooperative cancellation.

• id : PosNat
• action : IO Unit
• token : Std.CancellationToken

Scheduling

def Control.Concurrent.Scheduler.schedule (thread : GreenThread) : IO (Task (Except IO.Error Unit))

Submit a green thread to Lean's thread pool. Returns the Task that resolves when the action completes.

Uses IO.asTask with default priority (pooled, not dedicated). This means the work is queued onto the bounded thread pool instead of spawning a new OS thread. Millions of tasks can be queued — they are just closures on the heap until a pool worker picks them up.

Equations

• One or more equations did not get rendered due to their size.