Merge pull request #1343 from lean-ja/Seasawher/issue1333

plausibleのコード例にミス
lean-ja · Jan 17, 2025 · 79bab49 · 79bab49
2 parents 227e963 + d5bbb42
commit 79bab49
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/LeanByExample/Tactic/Plausible.lean b/LeanByExample/Tactic/Plausible.lean
@@ -114,5 +114,5 @@ deriving instance DecidableEq for MyNat
 /-- error: Found a counter-example! -/
 #guard_msgs in
   example : ∀ (a b : MyNat), a = b := by
-    -- `plausible` は最初使うことができない
+    -- `plausible` が使えるようになった！
     plausible (config := { quiet := true})