Merge pull request #1072 from lean-ja/update

バージョン更新

LeanByExample/Reference/Declarative/Class.lean

@@ -102,8 +102,9 @@ set_option pp.mvars false
 
 -- 返り値の型がわからないので型クラス解決ができないというエラーが出ている
 /--
-error: typeclass instance problem is stuck, it is often due to metavariables
-  Plus Nat (List Nat) ?_
+error: failed to synthesize
+  Plus Nat (List Nat) (IO ?_)
+Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #eval 1 +ₚ [1, 2]
 

LeanByExample/Reference/Declarative/Deriving.lean

@@ -11,16 +11,13 @@ inductive Color : Type where
   | green
   | blue
 
--- 最初は `Repr` が定義されていないので `eval` できない
+-- 暗黙的に Repr インスタンスを生成しない
+set_option eval.derive.repr false
+
+-- `Repr` が定義されていないので `eval` できない
 /--
-error: expression
-  Color.red
-has type
+error: could not synthesize a 'Repr' or 'ToString' instance for type
   Color
-but instance
-  Lean.Eval Color
-failed to be synthesized, this instance instructs Lean on how to display the resulting value,
-recall that any type implementing the `Repr` class also implements the `Lean.Eval` class
 -/
 #guard_msgs in #eval Color.red
 

LeanByExample/Reference/Diagnostic/Eval.lean

@@ -26,30 +26,17 @@ def main : IO Unit :=
 式の評価を行うコマンドであるため、型や関数など、評価のしようがないものを与えるとエラーになります。-/
 
 -- 型は評価できない
-/--
-error: expression
-  ℕ
-has type
-  Type
-but instance
-  Lean.MetaEval Type
-failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
--/
+/-- error: cannot evaluate, types are not computationally relevant -/
 #guard_msgs in #eval Nat
 
 -- 関数そのものも評価できない
 /--
-error: expression
-  fun x => x + 1
-has type
+error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
   ℕ → ℕ
-but instance
-  Lean.MetaEval (ℕ → ℕ)
-failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class
 -/
 #guard_msgs in #eval (fun x => x + 1)
 
-/- 一般に、[`Repr`](../TypeClass/Repr.md) や [`ToString`](../TypeClass/ToString.md) のインスタンスでないような型の項は `#eval` に渡すことができません。-/
+/- 一般に、[`Repr`](../TypeClass/Repr.md) や [`ToString`](../TypeClass/ToString.md) および `ToExpr` のインスタンスでないような型の項は `#eval` に渡すことができません。-/
 
 /- ## 例外処理の慣例
 Lean および Mathlib では、「関数ではなく定理に制約を付ける」ことが慣例です。

LeanByExample/Reference/Tactic/Exact.lean

@@ -2,6 +2,7 @@
 
 ゴールが `P` で、ローカルコンテキストに `hP : P` があるときに、`exact hP` はゴールを閉じます。`hP` がゴールの証明になっていないときには、失敗してエラーになります。-/
 variable (P Q : Prop)
+set_option linter.unusedVariables false in --#
 
 example (hP : P) (hQ : Q) : P := by
   -- `hQ : Q` は `P` の証明ではないのでもちろん失敗する

LeanByExample/Reference/Tactic/Rw.lean

@@ -51,7 +51,7 @@ example (h : a = b) (hb : a + 3 = 0) : b + 3 = 0 := by
 
 また、ゴールとローカルコンテキストの仮定 `h` に対して同時に書き換えたいときは `⊢` 記号を使って `rw [hPQ] at h ⊢` のようにします。-/
 
-example (h : a + 0 = a) (h1 : b + (a + 0) = b + a) (h2 : a + (a + 0) = a)
+example (h : a + 0 = a) (_h1 : b + (a + 0) = b + a) (_h2 : a + (a + 0) = a)
     : a + 0 = 0 + a := by
   -- ローカルコンテキストとゴールのすべてに対して書き換えを行う
   rw [h] at *

LeanByExample/Reference/Type/List.lean

@@ -142,7 +142,7 @@ example [Foldr α β] {a₁ a₂ a₃ : α} (init : β) :
 /- `List.foldl` と `List.foldr` の違いは、演算が左結合的と仮定するか右結合的と仮定するか以外にも、`List.foldl` は末尾再帰(tail recursion)であるが `List.foldr` はそうでないことが挙げられます。 -/
 
 /-- 自然数のリストの総和を計算する関数 -/
-def List.sum : List Nat → Nat
+def List.sum' : List Nat → Nat
   | [] => 0
   | n :: ns => n + sum ns
 

LeanByExample/Reference/TypeClass/HAdd.lean

@@ -11,10 +11,13 @@ structure Colour where
 
 def sample : Colour := { red := 2, blue := 4, green := 8 }
 
+-- メタ変数の番号を表示しない
+set_option pp.mvars false
+
 -- 最初は `+` 記号が定義されていないのでエラーになります。
 /--
 error: failed to synthesize
-  HAdd Colour Colour ?m.1653
+  HAdd Colour Colour ?_
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in #eval sample + sample

LeanByExample/Reference/TypeClass/Repr.lean

@@ -2,7 +2,7 @@
 # Repr
 `Repr` は、その型の項をどのように表示するかを指示する型クラスです。
 
-たとえば、以下のように新しく[構造体](../Declarative/Structure.md) `Point` を定義したとき、特に何も指定しなければ `Point` の項を `#eval` で表示することはできません。
+たとえば、以下のように新しく[構造体](../Declarative/Structure.md) `Point` を定義したとき、何も指定しなくても `Point` の項を `#eval` で表示することはできますが、裏で使用しているのが `Repr` インスタンスです。
 -/
 namespace Repr --#
 
@@ -14,19 +14,16 @@ structure Point (α : Type) : Type where
 -- 原点
 def origin : Point Nat := ⟨0, 0⟩
 
+-- Repr インスタンスを暗黙的に生成しない
+set_option eval.derive.repr false
+
 /--
-error: expression
-  origin
-has type
+error: could not synthesize a 'Repr' or 'ToString' instance for type
   Point Nat
-but instance
-  Lean.Eval (Point Nat)
-failed to be synthesized, this instance instructs Lean on how to display the resulting value,
-recall that any type implementing the `Repr` class also implements the `Lean.Eval` class
 -/
 #guard_msgs in #eval origin
 
-/- エラーメッセージが示すように、これは `Point` が型クラス `Lean.Eval` のインスタンスではないからです。エラーメッセージには、`Repr` クラスのインスタンスであれば自動的に `Lean.Eval` のインスタンスにもなることが書かれています。通常、`Lean.Eval` のインスタンスを手で登録することはなく、`Repr` インスタンスによって自動生成させます。
+/- エラーメッセージが示すように、`Point` が型クラス `Repr` または `ToString` のインスタンスではないため `#eval` が実行できずエラーになります。
 
 `Repr` インスタンスの登録方法ですが、通り一遍の表示で構わなければ [`deriving`](../Declarative/Deriving.md) コマンドで Lean に自動生成させることができます。-/
 
@@ -78,10 +75,7 @@ local instance [Repr α] : Repr (NestedList α) where
 #guard_msgs in #eval sample
 end --#
 
-/- あるいは、[`ToString`](./ToString.md) クラスのインスタンスがあればそこから `Lean.Eval` クラスのインスタンスも生成されて、表示に使われるので、それを利用しても良いでしょう。-/
-
--- `ToString` クラスのインスタンスがあれば、`Lean.Eval` のインスタンスが生成できる
-example {α : Type} [ToString α] : Lean.Eval α := inferInstance
+/- また、`Repr` インスタンスがなくても [`ToString`](./ToString.md) クラスのインスタンスがあればそれが表示に使われます。-/
 
 /-- `NestedList` を文字列に変換 -/
 partial def NestedList.toString [ToString α] : NestedList α → String

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4f5a57cc09c86b605511be02ca719f1499bc550e",
+   "rev": "97c8a350066b8a807d246b905abb690c1a15315b",
    "name": "«mk-exercise»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3500acfb8036a4e11b047ef14f52b5b1d315005b",
+   "rev": "d1585cbcb8a970d6fd68f2b7b68a7c6f6a8e33a2",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
+   "rev": "af731107d531b39cd7278c73f91c573f40340612",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d6ae727639429892c372d613b31967b6ee51f78c",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
+   "rev": "5dfdc66e0d503631527ad90c1b5d7815c86a8662",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "23268f52d3505955de3c26a42032702c25cfcbf8",
+   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.44",
+   "inputRev": "v0.0.46",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
+   "rev": "ac7b989cbf99169509433124ae484318e953d201",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d212dd74414e997653cd3484921f4159c955ccca",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fef6aa3e68311f7ddb82e3db00441493b0e6f39a",
+   "rev": "57f9c20e5c2160020f899520427b02d86d3ef96e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.14.0-rc2