wip

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

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)

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

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