#test

#test コマンドは、Plausible ライブラリで定義されているもので、与えられた命題が成り立つかどうか、具体例をランダムに生成してチェックすることで検証します。plausible タクティクと同様の機能を持ちます。

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