From 94ede53940a210fc9388ee4d0d7dcd67cdef04fb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Sep 2021 11:53:12 -0700
Subject: [PATCH] chore: use doc string

---
 src/Lean/Elab/PreDefinition/Basic.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 24375f497d..6681c7f5c3 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -13,9 +13,9 @@ namespace Lean.Elab
 open Meta
 open Term
 
-/-
-A (potentially recursive) definition.
-The elaborator converts it into Kernel definitions using many different strategies.
+/--
+  A (potentially recursive) definition.
+  The elaborator converts it into Kernel definitions using many different strategies.
 -/
 structure PreDefinition where
   ref         : Syntax