From 43f88007882aea9fcc946dbdd814ef7d4cd78c2f Mon Sep 17 00:00:00 2001
From: Peiyang Song <p_song@ucsb.edu>
Date: Mon, 1 Jul 2024 13:34:14 +0800
Subject: [PATCH] minor fix for premise selection doc format

---
 LeanCopilot/Tactics.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanCopilot/Tactics.lean b/LeanCopilot/Tactics.lean
index d2325d8..b7ada35 100644
--- a/LeanCopilot/Tactics.lean
+++ b/LeanCopilot/Tactics.lean
@@ -81,7 +81,7 @@ private def annotatePremise (pi : PremiseInfo) : MetaM String := do
     let premise_type ← Meta.ppExpr info.type
     let some doc_str ← findDocString? (← getEnv) declName
       | return s!"\n{pi.name} : {premise_type}"
-    return s!"\n{pi.name} : {premise_type}\n```doc\n{doc_str}```"
+    return s!"\n{pi.name} : {premise_type}\n```doc\n{doc_str}\n```"
   catch _ => return s!"\n{pi.name} needs to be imported from {pi.path}.\n```code\n{pi.code}\n```"