plausible のエラーメッセージの修正

lean-ja · Nov 4, 2024 · 172120b · 172120b
1 parent f6713e1
commit 172120b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/LeanByExample/Reference/Tactic/Plausible.lean b/LeanByExample/Reference/Tactic/Plausible.lean
@@ -8,7 +8,7 @@ variable (a b : Nat)
 #guard_msgs (drop warning) in --#
 example (h : 0 ≤ a + b) : 1 ≤ a := by
   /-
-  Found problems! というエラーが表示される
+  Found a counter-example! というエラーが表示される
   -/
   fail_if_success plausible