fix: docstring of ByteArray.IsValidUTF8.intro

Author: TwoFX

src/Init/Prelude.lean

@@ -3395,7 +3395,10 @@ Note that in order for this definition to be well-behaved it is necessary to kno
 is unique. To show this, one defines UTF-8 decoding and shows that encoding and decoding are
 mutually inverse. -/
 inductive ByteArray.IsValidUTF8 (b : ByteArray) : Prop
-  /-- Show that a byte -/
+  /--
+  Show that a byte array is valid UTF-8 by exhibiting it as `List.utf8Encode m` for some list `m`
+  of characters.
+   -/
   | intro (m : List Char) (hm : Eq b (List.utf8Encode m))
 
 /--