From 172120b47a09a46af96493bc461a636236329767 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 4 Nov 2024 16:59:58 +0900 Subject: [PATCH] =?UTF-8?q?`plausible`=20=E3=81=AE=E3=82=A8=E3=83=A9?= =?UTF-8?q?=E3=83=BC=E3=83=A1=E3=83=83=E3=82=BB=E3=83=BC=E3=82=B8=E3=81=AE?= =?UTF-8?q?=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Tactic/Plausible.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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