From 01fd9b7caab06e0c7d64bfc6fff9629c802263b6 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 11 Apr 2024 18:56:04 +0200
Subject: [PATCH] Update src/Init/Control/Basic.lean

---
 src/Init/Control/Basic.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index e9a5ba061489..2e3e7519bf2e 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -34,7 +34,10 @@ Important instances include
 class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1) v) where
   /-- See `Alternative`. -/
   failure : {α : Type u} → f α
-  /-- See `Alternative`. Can be writen using `<|>`.  -/
+  /--
+  Depending on the `Alternative` instance, collects values or recovers from `failure`s by
+  returning the leftmost success. Can be written using the `<|>` operator syntax.
+  -/
   orElse  : {α : Type u} → f α → (Unit → f α) → f α
 
 instance (f : Type u → Type v) (α : Type u) [Alternative f] : OrElse (f α) := ⟨Alternative.orElse⟩