From f5db3fb53ae281c10a3b319ecfc959e9bc30c18a Mon Sep 17 00:00:00 2001
From: Matt Russell <MattRussellUK@gmail.com>
Date: Sun, 1 Dec 2024 17:02:30 +0000
Subject: [PATCH] wip

---
 Aoc2024/Day01/Main.lean  |  1 +
 Aoc2024/Day01/Solve.lean |  8 ++++----
 Aoc2024/Utils.lean       | 11 +++++------
 notes.md                 |  3 ---
 4 files changed, 10 insertions(+), 13 deletions(-)

diff --git a/Aoc2024/Day01/Main.lean b/Aoc2024/Day01/Main.lean
index 20993e4..9af09f4 100644
--- a/Aoc2024/Day01/Main.lean
+++ b/Aoc2024/Day01/Main.lean
@@ -7,6 +7,7 @@ def solve (name: String) (inputPath: String) : IO Unit := do
   let input <- IO.FS.readFile inputPath
   IO.println s!"Part 1: {<- parseAndSolvePart1 input}"
   IO.println s!"Part 2: {<- parseAndSolvePart2 input}"
+
 def main : IO Unit := do
   IO.println "Day 1"
   IO.println ""
diff --git a/Aoc2024/Day01/Solve.lean b/Aoc2024/Day01/Solve.lean
index 7f48bdf..4ac20e4 100644
--- a/Aoc2024/Day01/Solve.lean
+++ b/Aoc2024/Day01/Solve.lean
@@ -6,17 +6,17 @@ namespace Aoc2024.Day01
 private def solvePart1 (pairs : List (Int × Int)) : Int :=
   let (firsts, seconds) := pairs.unzip
   let distance (a b : Int) : Int := (a - b).natAbs
-  firsts.mergeSort.zipWith distance seconds.mergeSort |> sumList
+  (firsts.mergeSort.zipWith distance seconds.mergeSort).sum
 
-def parseAndSolvePart1 : String -> Except String Int := .map solvePart1 ∘ parseLines
+def parseAndSolvePart1 (s : String): Except String Int := parseLines s |> .map solvePart1
 
 #guard (parseAndSolvePart1 exampleInput == Except.ok 11)
 
 private def solvePart2 (pairs : List (Int × Int)) : Int :=
   let (firsts, seconds) := pairs.unzip
   let similarityScore (n : Int) : Int := seconds.count n * n
-  firsts |> sumListBy similarityScore
+  firsts.sumBy similarityScore
 
-def parseAndSolvePart2 : String -> Except String Int := .map solvePart2 ∘ parseLines
+def parseAndSolvePart2 (s : String): Except String Int := parseLines s |> .map solvePart2
 
 #guard (parseAndSolvePart2 exampleInput == Except.ok 31)
diff --git a/Aoc2024/Utils.lean b/Aoc2024/Utils.lean
index 0f39d1b..e1d4898 100644
--- a/Aoc2024/Utils.lean
+++ b/Aoc2024/Utils.lean
@@ -2,15 +2,14 @@ import Std
 open Std.Internal.Parsec.String
 open Std.Internal.Parsec
 
-def sumList (nums : List Int) : Int := nums.foldl (· + ·) 0
+def List.sum (xs: List Int) : Int := xs.foldl .add 0
 
-#guard sumList [] = 0
-#guard sumList [1, 2, 3] = 6
+#guard [].sum = 0
+#guard [1, 2, 3].sum = 6
 
-def sumListBy (f : Int → Int) (nums : List Int) : Int :=
-  nums.foldl (fun acc x => acc + f x) 0
+def List.sumBy (f : α → Int) (xs : List α) : Int := xs.foldl (fun acc x => acc + f x) 0
 
-#guard sumListBy (fun x => x * x) [1, 2, 3] = 14
+#guard [1, 2, 3].sumBy (fun x => x * x) = 14
 
 -- https://brandonrozek.com/blog/writing-unit-tests-lean-4/
 def Except.deq [DecidableEq α] [DecidableEq β] : DecidableEq (Except α β) := by
diff --git a/notes.md b/notes.md
index aa9015a..2f1734e 100644
--- a/notes.md
+++ b/notes.md
@@ -4,9 +4,6 @@
 * https://github.com/anurudhp/aoc2022/blob/main/Aoc/Day02.lean
 
 ## Questions
-* Build different executables in Lakefile for each day?
-* Can I import just some symbols from a file rather than all of them? Can I alias on import?
-* Can I add functions to Option, List etc?
 * How does this syntax work?
     let [a, b] := l | throw s!"Expected two elements, but got {l.length}"