Module lean_sys::task

Tasks

Functions

lean_finalize_task_manager^⚠

lean_init_task_manager^⚠

lean_init_task_manager_using^⚠

lean_io_cancel_core^⚠

primitive for implementing IO.cancel : Task a -> IO Unit

lean_io_check_canceled_core^⚠

primitive for implementing IO.checkCanceled : IO Bool

lean_io_has_finished_core^⚠

primitive for implementing IO.hasFinished : Task a -> IO Unit

lean_io_wait_any_core^⚠

primitive for implementing IO.waitAny : List (Task a) -> IO (Task a)

lean_task_bind^⚠

Task.bind (x : Task A) (f : A -> Task B) (prio : Nat) : Task B

lean_task_bind_core^⚠

lean_task_get^⚠

lean_task_get_own^⚠

Primitive for implementing Task.get : Task A -> A

lean_task_map^⚠

Task.map (f : A -> B) (t : Task A) (prio : Nat) : Task B

lean_task_map_core^⚠

lean_task_pure^⚠

Convert a value a : A into Task A

lean_task_spawn^⚠

Run a closure Unit -> A as a Task A

lean_task_spawn_core^⚠