From 4bd2ba34abf5a7380d7bffe9da6ac7dc9dce6ea8 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Fri, 20 Dec 2024 23:34:53 +0900
Subject: [PATCH] =?UTF-8?q?`#test`=20=E3=82=B3=E3=83=9E=E3=83=B3=E3=83=89?=
 =?UTF-8?q?=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99=E3=82=8B=20Fixes=20#1169?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Diagnostic/Test.lean  | 12 ++++++++++++
 LeanByExample/Tactic/Plausible.lean |  2 ++
 booksrc/SUMMARY.md                  |  1 +
 3 files changed, 15 insertions(+)
 create mode 100644 LeanByExample/Diagnostic/Test.lean

diff --git a/LeanByExample/Diagnostic/Test.lean b/LeanByExample/Diagnostic/Test.lean
new file mode 100644
index 00000000..c8a1dfdd
--- /dev/null
+++ b/LeanByExample/Diagnostic/Test.lean
@@ -0,0 +1,12 @@
+/- # \#test
+`#test` コマンドは、Plausible ライブラリで定義されているもので、与えられた命題が成り立つかどうか、具体例をランダムに生成してチェックすることで検証します。[`plausible`](#{root}/Tactic/Plausible.md) タクティクと同様の機能を持ちます。
+-/
+import Plausible
+
+-- 命題 `P : Prop` に対して、`#test P` で `P` が成り立つかどうかを検証する
+#test ∀ (n : Nat), n + 0 = n
+
+-- 反例が見つからなければ「反例が見つからない」と教えてくれる
+/-- info: Unable to find a counter-example -/
+#guard_msgs in
+  #test ∀ (n : Nat), n + n = 2 * n
diff --git a/LeanByExample/Tactic/Plausible.lean b/LeanByExample/Tactic/Plausible.lean
index feeb5b17..2d217be3 100644
--- a/LeanByExample/Tactic/Plausible.lean
+++ b/LeanByExample/Tactic/Plausible.lean
@@ -27,6 +27,8 @@ warning: declaration uses 'sorry'
   example (a : Nat) : a ≠ a → a ≤ 1 := by
     plausible
 
+/- 同様の機能を持つコマンドとして [`#test`](#{root}/Diagnostic/Test.md) コマンドがあります。-/
+
 /- ## 引数
 引数として、オプションを渡すことができます。
 
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index a87f79dd..2268a94f 100644
--- a/booksrc/SUMMARY.md
+++ b/booksrc/SUMMARY.md
@@ -20,6 +20,7 @@
   - [#print: 中身を見る](./Diagnostic/Print.md)
   - [#reduce: 式を簡約する](./Diagnostic/Reduce.md)
   - [#synth: 型クラスの検査](./Diagnostic/Synth.md)
+  - [#test: プロパティベーステスト](./Diagnostic/Test.md)
   - [#time: 実行時間計測](./Diagnostic/Time.md)
   - [#version: バージョン表示](./Diagnostic/Version.md)
   - [#whnf: 式を弱頭正規形に](./Diagnostic/Whnf.md)