feat: hide grind auxiliary gadgets in messages (#6882)

This PR ensures `grind` auxiliary gadgets are "hidden" in error and
diagnostic messages.

src/Init/Grind/Util.lean

@@ -41,4 +41,22 @@ def MatchCond (p : Prop) : Prop := p
 theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (@nestedProof p hp) (@nestedProof q hq) := by
   subst h; apply HEq.refl
 
+@[app_unexpander nestedProof]
+def nestedProofUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $p:term) => `(‹$p›)
+  | _ => throw ()
+
+@[app_unexpander MatchCond]
+def matchCondUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $p:term) => `($p)
+  | _ => throw ()
+
+@[app_unexpander EqMatch]
+def eqMatchUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $lhs:term $rhs:term) => `($lhs = $rhs)
+  | _ => throw ()
+
 end Lean.Grind

tests/lean/run/grind_match1.lean

@@ -24,11 +24,10 @@ info: [grind.assert] (match as, bs with
 [grind.assert] a₁ :: f 0 = as
 [grind.assert] f 0 = a₂ :: f 1
 [grind.assert] ¬d = []
-[grind.assert] Lean.Grind.EqMatch
-      (match a₁ :: a₂ :: f 1, [] with
+[grind.assert] (match a₁ :: a₂ :: f 1, [] with
       | [], x => bs
       | head :: head_1 :: tail, [] => []
-      | x :: xs, ys => x :: g xs ys)
+      | x :: xs, ys => x :: g xs ys) =
       []
 [grind.split.resolved] match as, bs with
     | [], x => bs

tests/lean/run/grind_nested_proofs.lean

@@ -22,19 +22,15 @@ detect equalities between array access terms.
 -/
 
 /--
-info: [Meta.debug] [Lean.Grind.nestedProof (i < a.toList.length),
-     Lean.Grind.nestedProof (j < a.toList.length),
-     Lean.Grind.nestedProof (j < b.toList.length)]
+info: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›]
 [Meta.debug] [a[i], b[j], a[j]]
 -/
 #guard_msgs (info) in
 example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i ≤ j) : a[i] < a[j] + b[j] → i = j → a = b → False := by
   grind on_failure fallback
 
 /--
-info: [Meta.debug] [Lean.Grind.nestedProof (i < a.toList.length),
-     Lean.Grind.nestedProof (j < a.toList.length),
-     Lean.Grind.nestedProof (j < b.toList.length)]
+info: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›]
 [Meta.debug] [a[i], a[j]]
 -/
 #guard_msgs (info) in