diff --git a/LeanByExample/Reference/Tactic/Plausible.lean b/LeanByExample/Reference/Tactic/Plausible.lean index 7cd35e1..71349ca 100644 --- 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