From ed81967338992c52f2dbc33a574df9f0588e5fe1 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 22 Dec 2020 21:58:25 -0500
Subject: [PATCH] doc: AsyncList methods

---
 src/Lean/Server/AsyncList.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Server/AsyncList.lean b/src/Lean/Server/AsyncList.lean
index d54f3222e9..87a1ceebd5 100644
--- a/src/Lean/Server/AsyncList.lean
+++ b/src/Lean/Server/AsyncList.lean
@@ -62,8 +62,8 @@ partial def unfoldAsync [Coe Error ε] (f : α → ExceptT ε IO α)
   let tInit ← coeErr <$> asTask (step init)
   asyncTail tInit
 
-/-- Waits for the entire computation to finish and returns the computed
-list. If computation was ongoing, also returns the terminating value. -/
+/-- The computed, synchronous list. If an async tail was present, returns also
+its terminating value. -/
 partial def getAll : AsyncList ε α → List α × Option ε
   | cons hd tl =>
     let ⟨l, e?⟩ := tl.getAll
@@ -74,9 +74,9 @@ partial def getAll : AsyncList ε α → List α × Option ε
     | Except.ok tl => tl.getAll
     | Except.error e => ⟨[], some e⟩
 
-/-- Waits for the entire computation to finish and returns the computed
-list. If computation was ongoing, also returns the terminating value.
-As opposed to getAll, ensures that the waiting is completed. -/
+/-- An IO action which ensures that the async tail, if it exists,
+is fully executed. This is useful if the computation has side effects.
+Returns the same values as `getAll`. -/
 partial def waitAll : AsyncList ε α → IO (List α × Option ε)
   | cons hd tl => do
     let ⟨l, e?⟩ ← tl.waitAll
@@ -106,7 +106,7 @@ private partial def finishedPrefixAux : List α → AsyncList ε α → List α
   | acc, nil          => acc
   | acc, asyncTail tl => acc
 
-/-- The longest already-computed prefix of the stream. -/
+/-- The longest already-computed prefix of the list. -/
 def finishedPrefix : AsyncList ε α → List α :=
   List.reverse ∘ (finishedPrefixAux [])