Merge pull request #433 from lean-ja/update

Lean のバージョンを v4.10.0-rc1 に更新する

Examples/Command/Declarative/Opaque.lean

@@ -0,0 +1,11 @@
+/- # opaque -/
+
+opaque A : Type
+opaque B : Type
+opaque C : Type
+
+variable [Inhabited C]
+
+opaque f : (A → B) → C
+
+#check_failure f f

Examples/Command/Declarative/Partial.lean

@@ -14,21 +14,24 @@ namespace WithoutPartial --#
 error: fail to show termination for
   WithoutPartial.alternate
 with errors
-argument #2 was not used for structural recursion
+structural recursion cannot be used:
+
+argument #1 cannot be used for structural recursion
+  it is unchanged in the recursive calls
+
+argument #2 cannot be used for structural recursion
   failed to eliminate recursive application
     alternate ys xs
 
-argument #3 was not used for structural recursion
+argument #3 cannot be used for structural recursion
   failed to eliminate recursive application
     alternate ys xs
 
-structural recursion cannot be used
-
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             xs ys
-1) 38:24-39  ?  ?
+1) 41:24-39  ?  ?
 Please use `termination_by` to specify a decreasing measure.
 -/
 #guard_msgs (whitespace := lax) in

Examples/Command/Declarative/TerminationBy.lean

@@ -7,12 +7,12 @@ namespace TerminationBy --#
 error: fail to show termination for
   TerminationBy.M
 with errors
-argument #1 was not used for structural recursion
+structural recursion cannot be used:
+
+argument #1 cannot be used for structural recursion
   failed to eliminate recursive application
     M (n + 11)
 
-structural recursion cannot be used
-
 failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation

Examples/Command/Diagnostic/Print.lean

@@ -27,7 +27,7 @@ fun n m => rfl
 /-- 排中律 -/
 example : ∀ (p : Prop), p ∨ ¬p := Classical.em
 
-/-- info: 'Classical.em' depends on axioms: [Classical.choice, propext, Quot.sound] -/
+/-- info: 'Classical.em' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in
 #print axioms Classical.em
 

Examples/Tactic/ITauto.lean

@@ -19,5 +19,5 @@ theorem not_iff_not₁ (p : Prop) : ¬ (p ↔ ¬ p) := by tauto
 #guard_msgs in #print axioms not_iff_not₀
 
 -- 勝手に選択原理を使用している！
-/-- info: 'not_iff_not₁' depends on axioms: [Classical.choice, propext, Quot.sound] -/
+/-- info: 'not_iff_not₁' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms not_iff_not₁

Examples/Tactic/Tauto.lean

@@ -36,7 +36,7 @@ example : ¬(∀ x, S x) → (∃ x, ¬ S x) := by
 theorem not_neg_iff {P : Prop} : ¬ (P ↔ ¬ P) := by tauto
 
 -- 選択原理を使っているが，これは排中律を使っているため
-/-- info: 'Tauto.not_neg_iff' depends on axioms: [Classical.choice, propext, Quot.sound] -/
+/-- info: 'Tauto.not_neg_iff' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms not_neg_iff
 
 -- 実際には排中律は必要ない

lake-manifest.json

@@ -1,9 +1,10 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/Seasawher/mdgen",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "e705093e3cc1dbfd7f6ac8732ce19b395dccf272",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
@@ -13,7 +14,8 @@
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
+   "scope": "leanprover-community",
+   "rev": "bba0af6e930ebcbabfacf021b21dd881d58aaa9d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,6 +24,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
+   "scope": "leanprover-community",
    "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
@@ -31,7 +34,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc",
+   "scope": "leanprover-community",
+   "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -40,25 +44,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.38",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71",
+   "scope": "leanprover-community",
+   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -67,10 +74,11 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab",
+   "scope": "",
+   "rev": "5d74b273dd4c171c1f57a2d75abc1d3e27d7095a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.9.0",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«Lean by Example»",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.10.0-rc1