version update

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

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

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

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

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

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"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0-rc4
+leanprover/lean4:v4.15.0-rc1