version 更新

Author: Seasawher

LeanByExample/Reference/Diagnostic/Help.lean

@@ -11,7 +11,7 @@
 
 他にも機能がありますが、詳細は[Mathlib のドキュメント](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/HelpCmd.html)をご覧ください。
 -/
-import Mathlib.Tactic
+import Batteries.Tactic.HelpCmd
 
 -- 以下のコマンドで全 tactic のリストが見られます
 #help tactic

LeanByExample/Reference/Tactic/SlimCheck.lean renamed to LeanByExample/Reference/Tactic/Plausible.lean

@@ -1,16 +1,16 @@
-/- # slim_check
+/- # plausible
 
-`slim_check` は、証明しようとしているゴールが間違っていないかチェックし、反例を見つけるとエラーで警告するタクティクです。 -/
-import Mathlib.Tactic.SlimCheck
+`plausible` は、証明しようとしているゴールが間違っていないかチェックし、反例を見つけるとエラーで警告するタクティクです。 -/
+import Plausible
 
-variable (a b : ℕ)
+variable (a b : Nat)
 
 #guard_msgs (drop warning) in --#
 example (h : 0 ≤ a + b) : 1 ≤ a := by
   /-
   Found problems! というエラーが表示される
   -/
-  fail_if_success slim_check
+  fail_if_success plausible
 
   sorry
 
@@ -22,4 +22,4 @@ example (h : 0 ≤ a + b) : 1 ≤ a := by
 -- Gave up ** times と表示される
 #guard_msgs (drop warning) in --#
 example (h : a = 1) : a ≤ 1 := by
-  slim_check
+  plausible

booksrc/SUMMARY.md

@@ -170,7 +170,7 @@
   - [show: 示すべきことを宣言](./Reference/Tactic/Show.md)
   - [simp_all: 仮定とゴールを全て単純化](./Reference/Tactic/SimpAll.md)
   - [simp: 単純化](./Reference/Tactic/Simp.md)
-  - [slim_check: 反例を見つける](./Reference/Tactic/SlimCheck.md)
+  - [plausible: 反例を見つける](./Reference/Tactic/Plausible.md)
   - [sorry: 証明したことにする](./Reference/Tactic/Sorry.md)
   - [split: if/match 式を分解](./Reference/Tactic/Split.md)
   - [suffices: 十分条件に帰着](./Reference/Tactic/Suffices.md)

lake-manifest.json

@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb6c831c05bc6ca6d37454ca97531a9b780dfcb5",
+   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
+   "rev": "d6ae727639429892c372d613b31967b6ee51f78c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c",
+   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
+   "rev": "23268f52d3505955de3c26a42032702c25cfcbf8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.43",
+   "inputRev": "v0.0.44",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c1970bea80ac3357a6a991a6d00d12e7435c12c7",
+   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -91,11 +91,21 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d212dd74414e997653cd3484921f4159c955ccca",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4b5f1a09a2e4d4d693db48703e230c11782c3c5e",
+   "rev": "fef6aa3e68311f7ddb82e3db00441493b0e6f39a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc3
+leanprover/lean4:v4.13.0