chore: add some missing docs

leanprover · Nov 7, 2024 · 0348811 · 0348811
1 parent b473580
commit 0348811
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
@@ -363,9 +363,10 @@ end SerialMessage
 
 namespace Message
 
-abbrev kind (msg : Message) :=
+@[inherit_doc MessageData.kind] abbrev kind (msg : Message) :=
   msg.data.kind
 
+/-- Serializes the message, converting its data into a string and saving its kind. -/
 @[inline] def serialize (msg : Message) : IO SerialMessage := do
   return {msg with kind := msg.kind, data := ← msg.data.toString}