Update src/Init/Control/Basic.lean

src/Init/Control/Basic.lean

@@ -34,7 +34,10 @@ Error recovery and state can interact subtly. For example, the implementation of
 -- NB: List instance is in mathlib. Once upstreamed, add
 -- * `List`, where `failure` is the empty list and `<|>` concatenates.
 class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1) v) where
-  /-- See `Alternative`. -/
+  /--
+  Produces an empty collection or recoverable failure.  The `<|>` operator collects values or recovers
+  from failures. See `Alternative` for more details.
+  -/
   failure : {α : Type u} → f α
   /--
   Depending on the `Alternative` instance, collects values or recovers from `failure`s by