From cc5007d05105d73805f43b381feea2d816e56d2a Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Thu, 5 Dec 2024 20:30:56 +0900
Subject: [PATCH] version update

---
 Src/Problem27.lean | 15 ++++++++++-----
 Src/Problem48.lean | 12 +++++++++---
 Src/Problem55.lean | 12 +++++++++---
 Src/Problem58.lean | 12 +++++++++---
 Src/Problem59.lean | 12 +++++++++---
 lake-manifest.json | 24 ++++++++++++------------
 lean-toolchain     |  2 +-
 7 files changed, 59 insertions(+), 30 deletions(-)

diff --git a/Src/Problem27.lean b/Src/Problem27.lean
index e769b77..7c12352 100644
--- a/Src/Problem27.lean
+++ b/Src/Problem27.lean
@@ -8,13 +8,18 @@ Write a function that generates all the possibilities and returns them in a list
 universe u
 variable {α : Type}
 
-/-- `List` is a Monad.
-Since Lean does not use lazy evaluation, no Monad instance of List is defined in the Lean standard library for performance reasons. -/
-instance : Monad List.{u} where
-  pure := @List.pure
-  bind := @List.bind
+namespace ListMonad
+
+/-- monad instance of `List` -/
+scoped instance : Monad List where
+  pure := fun {_} a => [a]
+  bind := @List.flatMap
   map := @List.map
 
+end ListMonad
+
+open scoped ListMonad
+
 def List.split (n : Nat) (xs : List α) : List (List α × List α) :=
   -- sorry
   match n, xs with
diff --git a/Src/Problem48.lean b/Src/Problem48.lean
index d771b0a..1dabf44 100644
--- a/Src/Problem48.lean
+++ b/Src/Problem48.lean
@@ -5,12 +5,18 @@ Generalize Problem 47 in such a way that the logical expression may contain any
 -/
 universe u
 
+namespace ListMonad
+
 /-- monad instance of `List` -/
-instance : Monad List.{u} where
-  pure := @List.pure
-  bind := @List.bind
+scoped instance : Monad List.{u} where
+  pure := fun {_} a => [a]
+  bind := @List.flatMap
   map := @List.map
 
+end ListMonad
+
+open scoped ListMonad
+
 def Arity : (n : Nat) → Type
   | 0 => Bool
   | n + 1 => Bool → Arity n
diff --git a/Src/Problem55.lean b/Src/Problem55.lean
index 38d81d4..fa6100e 100644
--- a/Src/Problem55.lean
+++ b/Src/Problem55.lean
@@ -26,12 +26,18 @@ def BinTree.isCBalanced {α : Type} : BinTree α → Bool
   | .node _ l r =>
     Int.natAbs ((l.nodes : Int) - (r.nodes : Int)) ≤ 1 && l.isCBalanced && r.isCBalanced
 
+namespace ListMonad
+
 /-- monad instance of `List` -/
-instance : Monad List where
-  pure := @List.pure
-  bind := @List.bind
+scoped instance : Monad List where
+  pure := fun {_} a => [a]
+  bind := @List.flatMap
   map := @List.map
 
+end ListMonad
+
+open scoped ListMonad
+
 /-- construct all completely balanced binary trees which contains `x` elements -/
 partial def cbalTree (x : Nat) : List (BinTree Unit) :=
   -- sorry
diff --git a/Src/Problem58.lean b/Src/Problem58.lean
index 1f0beea..ab52a9c 100644
--- a/Src/Problem58.lean
+++ b/Src/Problem58.lean
@@ -42,12 +42,18 @@ end
 
 #eval BinTree.node 'x' (leaf 'x') .empty
 
+namespace ListMonad
+
 /-- monad instance of `List` -/
-instance : Monad List where
-  pure := @List.pure
-  bind := @List.bind
+scoped instance : Monad List where
+  pure := fun {_} a => [a]
+  bind := @List.flatMap
   map := @List.map
 
+end ListMonad
+
+open scoped ListMonad
+
 /-- construct all balanced binary trees which contains `x` elements -/
 partial def cbalTree (x : Nat) : List (BinTree Unit) :=
   -- sorry
diff --git a/Src/Problem59.lean b/Src/Problem59.lean
index 4e122ab..36b6415 100644
--- a/Src/Problem59.lean
+++ b/Src/Problem59.lean
@@ -19,12 +19,18 @@ def BinTree.height (t : BinTree α) : Nat :=
   | .empty => 0
   | .node _ l r => 1 + max l.height r.height
 
+namespace ListMonad
+
 /-- monad instance of `List` -/
-instance : Monad List where
-  pure := @List.pure
-  bind := @List.bind
+scoped instance : Monad List where
+  pure := fun {_} a => [a]
+  bind := @List.flatMap
   map := @List.map
 
+end ListMonad
+
+open scoped ListMonad
+
 /-- construct all balanced binary trees which contains `x` elements -/
 partial def cbalTree (x : Nat) : List (BinTree Unit) :=
   -- sorry
diff --git a/lake-manifest.json b/lake-manifest.json
index d55df9e..674ec58 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/Seasawher/mk-exercise",
+ [{"url": "https://github.com/Seasawher/mdgen",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "ebaada203996d763d17fbdda6a1da6c9cb55f1ad",
+   "name": "mdgen",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/Seasawher/mk-exercise",
    "type": "git",
    "subDir": null,
    "scope": "",
@@ -20,16 +30,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/Seasawher/mdgen",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "d1585cbcb8a970d6fd68f2b7b68a7c6f6a8e33a2",
-   "name": "mdgen",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.toml"}],
  "name": "lean99",
  "lakeDir": ".lake"}
diff --git a/lean-toolchain b/lean-toolchain
index a254364..cf25a98 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc4
+leanprover/lean4:v4.15.0-rc1