chore: fix message

leanprover · Jan 14, 2025 · a0de63e · a0de63e
1 parent fb11fef
commit a0de63e
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 33 deletions.
diff --git a/src/Lean/Meta/Tactic/Grind/PP.lean b/src/Lean/Meta/Tactic/Grind/PP.lean
@@ -96,12 +96,12 @@ private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
    if let some trueEqc := trueEqc? then result := result.push trueEqc
    if let some falseEqc := falseEqc? then result := result.push falseEqc
    unless otherEqcs.isEmpty do
-     result := result.push <| .trace { cls := `eqc } "equivalence classes" otherEqcs
+     result := result.push <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
    return result
 
 def goalToMessageData (goal : Goal) : MetaM MessageData := goal.mvarId.withContext do
   let mut m : Array MessageData := #[.ofGoal goal.mvarId]
-  m := m.push <| ppExprArray `facts "asserted facts" goal.facts.toArray `prop
+  m := m.push <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
   m := m ++ (← ppEqcs goal)
   addMessageContextFull <| MessageData.joinSep m.toList ""
 

diff --git a/tests/lean/run/grind_erase_attr.lean b/tests/lean/run/grind_erase_attr.lean
@@ -24,19 +24,15 @@ example : f (f (f a)) = f a := by
 attribute [-grind] fthm
 
 /--
-error: `grind` failed
-case grind
+error: unsolved goals
 a : Nat
-x✝ : ¬f (f (f a)) = f a
-⊢ False[facts] asserted facts
-  [prop] ¬f (f (f a)) = f a[eqc] False propositions
-  [prop] f (f (f a)) = f a
+⊢ f (f (f a)) = f a
 ---
 info: [grind.assert] ¬f (f (f a)) = f a
 -/
 #guard_msgs (info, error) in
 example : f (f (f a)) = f a := by
-  grind
+  fail_if_success grind
 
 /--
 error: `fthm` is not marked with the `[grind]` attribute
@@ -62,27 +58,17 @@ example : g a = b → a = 0 → b = 1 := by
 attribute [-grind] g
 
 /--
-error: `grind` failed
-case grind
+error: unsolved goals
 a b : Nat
-a✝¹ : g a = b
-a✝ : a = 0
-x✝ : ¬b = 1
-⊢ False[facts] asserted facts
-  [prop] g a = b
-  [prop] a = 0
-  [prop] ¬b = 1[eqc] False propositions
-  [prop] b = 1[eqc] equivalence classes
-  [eqc] {a, 0}
-  [eqc] {g a, b}
+⊢ g a = b → a = 0 → b = 1
 ---
 info: [grind.assert] g a = b
 [grind.assert] a = 0
 [grind.assert] ¬b = 1
 -/
 #guard_msgs (info, error) in
 example : g a = b → a = 0 → b = 1 := by
-  grind
+  fail_if_success grind
 
 /--
 error: `g` is not marked with the `[grind]` attribute

diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
@@ -13,7 +13,7 @@ left : p
 right : q
 h✝ : b = false
 h : c = true
-⊢ False[facts] asserted facts
+⊢ False[facts] Asserted facts
   [prop] a = true
   [prop] b = true ∨ c = true
   [prop] p
@@ -26,7 +26,7 @@ h : c = true
   [prop] q
   [prop] b = false ∨ a = false
   [prop] b = false
-  [prop] c = true[eqc] equivalence classes
+  [prop] c = true[eqc] Equivalence classes
   [eqc] {b = true, a = false}
   [eqc] {b, false}
   [eqc] {a, c, true}
@@ -46,14 +46,14 @@ h✝ : c = true
 left : p
 right : q
 h : b = false
-⊢ False[facts] asserted facts
+⊢ False[facts] Asserted facts
   [prop] a = true
   [prop] c = true
   [prop] p
   [prop] q
   [prop] b = false[eqc] True propositions
   [prop] p
-  [prop] q[eqc] equivalence classes
+  [prop] q[eqc] Equivalence classes
   [eqc] {b, false}
   [eqc] {a, c, true}
 -/
@@ -70,7 +70,7 @@ i j : Nat
 h : j + 1 < i + 1
 h✝ : j + 1 ≤ i
 x✝ : ¬g (i + 1) j ⋯ = i + j + 1
-⊢ False[facts] asserted facts
+⊢ False[facts] Asserted facts
   [prop] j + 1 ≤ i
   [prop] ¬g (i + 1) j ⋯ = i + j + 1[eqc] True propositions
   [prop] j + 1 ≤ i[eqc] False propositions
@@ -99,11 +99,11 @@ head_eq : a₁ = b₁
 x_eq : a₂ = b₂
 y_eq : a₃ = b₃
 tail_eq : as = bs
-⊢ False[facts] asserted facts
+⊢ False[facts] Asserted facts
   [prop] a₁ = b₁
   [prop] a₂ = b₂
   [prop] a₃ = b₃
-  [prop] as = bs[eqc] equivalence classes
+  [prop] as = bs[eqc] Equivalence classes
   [eqc] {as, bs}
   [eqc] {a₃, b₃}
   [eqc] {a₂, b₂}
@@ -130,7 +130,7 @@ h₂ : HEq q a
 h₃ : p = r
 left : ¬p ∨ r
 h : ¬r
-⊢ False[facts] asserted facts
+⊢ False[facts] Asserted facts
   [prop] HEq p a
   [prop] HEq q a
   [prop] p = r
@@ -155,7 +155,7 @@ h₂ : HEq q a
 h₃ : p = r
 left : ¬p ∨ r
 h : p
-⊢ False[facts] asserted facts
+⊢ False[facts] Asserted facts
   [prop] HEq p a
   [prop] HEq q a
   [prop] p = r

diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
@@ -244,7 +244,7 @@ case grind
 p q : Prop
 a✝¹ : p = q
 a✝ : p
-⊢ False[facts] asserted facts
+⊢ False[facts] Asserted facts
   [prop] p = q
   [prop] p[eqc] True propositions
   [prop] p = q
@@ -262,7 +262,7 @@ case grind
 p q : Prop
 a✝¹ : p = ¬q
 a✝ : p
-⊢ False[facts] asserted facts
+⊢ False[facts] Asserted facts
   [prop] p = ¬q
   [prop] p[eqc] True propositions
   [prop] p = ¬q