バージョン更新

lean-ja · Dec 7, 2024 · 588a32a · 588a32a
1 parent b21b578
commit 588a32a
Show file tree

Hide file tree

Showing 9 changed files with 74 additions and 76 deletions.
diff --git a/LeanByExample/Reference/Declarative/Syntax.lean b/LeanByExample/Reference/Declarative/Syntax.lean
@@ -71,8 +71,6 @@ local macro_rules
 
 #guard (3 - 5 + 4 = 2 as Int)
 
-#guard (2 * 3 / 2 = 3 as Rat)
-
 end --#
 /- ## name 構文
 `(name := ...)` という構文により、名前を付けることができます。名前を付けると、その名前で `Lean.ParserDescr` の項が生成されます。

diff --git a/LeanByExample/Reference/Type/Array.lean b/LeanByExample/Reference/Type/Array.lean
@@ -14,12 +14,12 @@ import Lean --#
 `Array α` は次のように連結リスト `List α` のラッパーとして定義されているように見えます。-/
 --#--
 /--
-info: structure Array.{u} : Type u → Type u
+info: structure Array.{u} (α : Type u) : Type u
 number of parameters: 1
-constructor:
-Array.mk : {α : Type u} → List α → Array α
 fields:
-toList : List α
+  Array.toList : List α
+constructor:
+  Array.mk.{u} {α : Type u} (toList : List α) : Array α
 -/
 #guard_msgs in #print Array
 --#--

diff --git a/LeanByExample/Reference/Type/Char.lean b/LeanByExample/Reference/Type/Char.lean
@@ -18,11 +18,11 @@
 /--
 info: structure Char : Type
 number of parameters: 0
-constructor:
-Char.mk : (val : UInt32) → val.isValidChar → Char
 fields:
-val : UInt32
-valid : self.val.isValidChar
+  Char.val : UInt32
+  Char.valid : self.val.isValidChar
+constructor:
+  Char.mk (val : UInt32) (valid : val.isValidChar) : Char
 -/
 #guard_msgs in #print Char
 --#--

diff --git a/LeanByExample/Reference/Type/String.lean b/LeanByExample/Reference/Type/String.lean
@@ -9,10 +9,10 @@ import Lean --#
 /--
 info: structure String : Type
 number of parameters: 0
-constructor:
-String.mk : List Char → String
 fields:
-data : List Char
+  String.data : List Char
+constructor:
+  String.mk (data : List Char) : String
 -/
 #guard_msgs in #print String
 --#--

diff --git a/LeanByExample/Reference/TypeClass/Functor.lean b/LeanByExample/Reference/TypeClass/Functor.lean
@@ -7,14 +7,14 @@
 namespace Hidden --#
 --#--
 /--
-info: class Functor.{u, v} : (Type u → Type v) → Type (max (u + 1) v)
+info: class Functor.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
 number of parameters: 1
-constructor:
-Functor.mk : {f : Type u → Type v} →
-  ({α β : Type u} → (α → β) → f α → f β) → ({α β : Type u} → α → f β → f α) → Functor f
 fields:
-map : {α β : Type u} → (α → β) → f α → f β
-mapConst : {α β : Type u} → α → f β → f α
+  Functor.map : {α β : Type u} → (α → β) → f α → f β
+  Functor.mapConst : {α β : Type u} → α → f β → f α
+constructor:
+  Functor.mk.{u, v} {f : Type u → Type v} (map : {α β : Type u} → (α → β) → f α → f β)
+    (mapConst : {α β : Type u} → α → f β → f α) : Functor f
 -/
 #guard_msgs in #print Functor
 --#--

diff --git a/LeanByExample/Reference/TypeClass/Inhabited.lean b/LeanByExample/Reference/TypeClass/Inhabited.lean
@@ -17,7 +17,7 @@ variable {α : Type} [Inhabited α]
 
 def get (a : Array α) (i : Nat) : α :=
   if h : i < a.size then
-    a.get ⟨i, h⟩
+    a.get i h
   else
     panic! "index out of bounds"
 

diff --git a/LeanByExample/Reference/TypeClass/LawfulFunctor.lean b/LeanByExample/Reference/TypeClass/LawfulFunctor.lean
@@ -12,17 +12,17 @@
 --#--
 -- # LawfulFunctor の仕様変更を監視するためのコード
 /--
-info: class LawfulFunctor.{u, v} : (f : Type u → Type v) → [inst : Functor f] → Prop
+info: class LawfulFunctor.{u, v} (f : Type u → Type v) [Functor f] : Prop
 number of parameters: 2
-constructor:
-LawfulFunctor.mk : ∀ {f : Type u → Type v} [inst : Functor f],
-  (∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β) →
-    (∀ {α : Type u} (x : f α), id <$> x = x) →
-      (∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x) → LawfulFunctor f
 fields:
-map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
-id_map : ∀ {α : Type u} (x : f α), id <$> x = x
-comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x
+  LawfulFunctor.map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
+  LawfulFunctor.id_map : ∀ {α : Type u} (x : f α), id <$> x = x
+  LawfulFunctor.comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x
+constructor:
+  LawfulFunctor.mk.{u, v} {f : Type u → Type v} [Functor f]
+    (map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β)
+    (id_map : ∀ {α : Type u} (x : f α), id <$> x = x)
+    (comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x) : LawfulFunctor f
 -/
 #guard_msgs in #print LawfulFunctor
 --#--

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,115 +1,115 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/lean4-cli.git",
+ [{"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
-   "name": "Cli",
+   "rev": "653f17d0c439d2d9d55797995521660adc6df994",
+   "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/Seasawher/mk-exercise.git",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/Seasawher/mdgen",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "97c8a350066b8a807d246b905abb690c1a15315b",
-   "name": "«mk-exercise»",
+   "rev": "ebaada203996d763d17fbdda6a1da6c9cb55f1ad",
+   "name": "mdgen",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/Seasawher/mdgen",
+  {"url": "https://github.com/Seasawher/mk-exercise.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d1585cbcb8a970d6fd68f2b7b68a7c6f6a8e33a2",
-   "name": "mdgen",
+   "rev": "ff99a9be9854683448f745835ddf09fb5d800f9b",
+   "name": "«mk-exercise»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/batteries",
+  {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c933dd9b00271d869e22b802a015092d1e8e454a",
-   "name": "batteries",
+   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
+   "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/quote4",
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
-   "name": "Qq",
+   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/aesop",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "de91b59101763419997026c35a41432ac8691f15",
-   "name": "aesop",
+   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.15.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
+   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.46",
+   "inputRev": "v0.0.48",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph",
+  {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
-   "name": "importGraph",
+   "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
+   "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+  {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
-   "name": "LeanSearchClient",
+   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
+   "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.14.0",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/plausible",
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
-   "name": "plausible",
+   "rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+  {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "53a5bce08b5099841ffdd06a32c37340fcd2e47a",
-   "name": "mathlib",
+   "scope": "leanprover",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
  "name": "«Lean by Example»",
  "lakeDir": ".lake"}
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc2
+leanprover/lean4:v4.15.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.14.0-rc2
		leanprover/lean4:v4.15.0-rc1