From aa17466a2a096ba44e2b067826c33c8a8baa6861 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 13 Jan 2025 13:04:58 +0100 Subject: [PATCH] Apply suggestions from code review Co-authored-by: Markus Himmel --- src/Std/Internal/Async/Basic.lean | 2 +- src/Std/Internal/Async/Timer.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Std/Internal/Async/Basic.lean b/src/Std/Internal/Async/Basic.lean index 387bdc8f22b00..cbab3ed68d112 100644 --- a/src/Std/Internal/Async/Basic.lean +++ b/src/Std/Internal/Async/Basic.lean @@ -32,7 +32,7 @@ instance : Pure AsyncTask where /-- Create a new `AsyncTask` that will run after `x` has finished. If `x`: -- errors, return an `AsyncTask` that reolves to the error. +- errors, return an `AsyncTask` that resolves to the error. - succeeds, run `f` on the result of `x` and return the `AsyncTask` produced by `f`. -/ @[inline] diff --git a/src/Std/Internal/Async/Timer.lean b/src/Std/Internal/Async/Timer.lean index 72cf604fb775a..5524fb2b7f66a 100644 --- a/src/Std/Internal/Async/Timer.lean +++ b/src/Std/Internal/Async/Timer.lean @@ -56,7 +56,7 @@ def reset (s : Sleep) : IO Unit := /-- If: -- `s` is still running this stops `s` without resolving any remaing `AsyncTask` that were created +- `s` is still running this stops `s` without resolving any remaining `AsyncTask`s that were created through `wait`. Note that if another `AsyncTask` is binding on any of these it is going hang forever without further intervention. - `s` is not yet or not anymore running this is a no-op.