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)