minor update

lean-dojo · Dec 7, 2023 · 79e41c9 · 79e41c9
1 parent 021797a
commit 79e41c9
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/LeanCopilot/Tactics.lean b/LeanCopilot/Tactics.lean
@@ -52,9 +52,9 @@ def annotatePremise (premisesWithInfoAndScores : String × String × String × F
  let info ← getConstInfo declName
  let premise_type ← Meta.ppExpr info.type
  let some doc_str ← findDocString? (← getEnv) declName
- | return s!"\n{premise} : {premise_type}\n"
- return s!"\n{premise} : {premise_type}\n\n```doc{doc_str}```"
- catch _ => return s!"\n{premise} needs to be imported from {path}.\n\n```code\n{code}\n```"
+ | return s!"\n{premise} : {premise_type}"
+ return s!"\n{premise} : {premise_type}\n```doc\n{doc_str}```"
+ catch _ => return s!"\n{premise} needs to be imported from {path}.\n```code\n{code}\n```"
 
 
 def retrieve (input : String) : TacticM (Array (String × String × String × Float)) := do