From c3bd1acf7fba96160bf62658a401d1695254ff05 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 7 Dec 2023 11:37:37 +0000
Subject: [PATCH] chore: add indents to guard_target and friends (#426)

---
 Std/Tactic/GuardExpr.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/Std/Tactic/GuardExpr.lean b/Std/Tactic/GuardExpr.lean
index 7765ce097e..c795674282 100644
--- a/Std/Tactic/GuardExpr.lean
+++ b/Std/Tactic/GuardExpr.lean
@@ -143,7 +143,8 @@ def evalGuardTarget : Tactic :=
     let t ← getTgt >>= instantiateMVars
     let r ← elabTerm r (← inferType t)
     let some mk := equal.toMatchKind eq | throwUnsupportedSyntax
-    unless ← mk.isEq r t do throwError "target of main goal is {t}, not {r}"
+    unless ← mk.isEq r t do
+      throwError "target of main goal is{indentExpr t}\nnot{indentExpr r}"
   fun
   | `(tactic| guard_target $eq $r) => go eq r getMainTarget
   | `(conv| guard_target $eq $r) => go eq r Conv.getLhs
@@ -181,7 +182,8 @@ def evalGuardHyp : Tactic := fun
       let some mk := colon.toMatchKind c | throwUnsupportedSyntax
       let e ← elabTerm p none
       let hty ← instantiateMVars lDecl.type
-      unless ← mk.isEq e hty do throwError m!"hypothesis {h} has type {hty}, not {e}"
+      unless ← mk.isEq e hty do
+        throwError m!"hypothesis {h} has type{indentExpr hty}\nnot{indentExpr e}"
     match lDecl.value?, val with
     | none, some _        => throwError m!"{h} is not a let binding"
     | some _, none        => throwError m!"{h} is a let binding"
@@ -189,7 +191,8 @@ def evalGuardHyp : Tactic := fun
       let some mk := eq.bind colonEq.toMatchKind | throwUnsupportedSyntax
       let e ← elabTerm val lDecl.type
       let hval ← instantiateMVars hval
-      unless ← mk.isEq e hval do throwError m!"hypothesis {h} has value {hval}, not {e}"
+      unless ← mk.isEq e hval do
+        throwError m!"hypothesis {h} has value{indentExpr hval}\nnot{indentExpr e}"
     | none, none          => pure ()
   | _ => throwUnsupportedSyntax