wip

Aoc2024/Day01/Parser.lean

@@ -4,7 +4,7 @@ def splitOnWhitespace (s : String) : List String :=
   s.split Char.isWhitespace |> .filter (· ≠ "")
 
 def parseNumber (s: String) : Except String Int :=
-  s.toInt? |> getOrExcept s!"Failed to parse as number: {s}"
+  s.toInt? |> getOrThrow s!"Failed to parse as number: {s}"
 
 def getTwoElements (l : List α) : Except String (α × α) := do
   let [a, b] := l | throw s!"Expected two elements, but got {l.length}"

Aoc2024/Utils.lean

@@ -1,23 +1,41 @@
 def sumList (nums : List Int) : Int := nums.foldl (· + ·) 0
 
-#guard (sumList [] == 0)
-#guard (sumList [1, 2, 3] == 6)
+#guard sumList [] = 0
+#guard sumList [1, 2, 3] = 6
 
 def sumListBy (f : Int → Int) (nums : List Int) : Int :=
   nums.foldl (fun acc x => acc + f x) 0
 
-#guard (sumListBy (fun x => x * x) [1, 2, 3] == 14)
+#guard sumListBy (fun x => x * x) [1, 2, 3] = 14
 
-instance [BEq α] : BEq (Except String α) where
+-- https://brandonrozek.com/blog/writing-unit-tests-lean-4/
+def Except.deq [DecidableEq α] [DecidableEq β] : DecidableEq (Except α β) := by
+  unfold DecidableEq
+  intro a b
+  cases a <;> cases b <;>
+  -- Get rid of obvious cases where .ok != .err
+  try { apply isFalse ; intro h ; injection h }
+  case error.error c d =>
+    match decEq c d with
+      | isTrue h => apply isTrue (by rw [h])
+      | isFalse _ => apply isFalse (by intro h; injection h; contradiction)
+  case ok.ok c d =>
+    match decEq c d with
+      | isTrue h => apply isTrue (by rw [h])
+      | isFalse _ => apply isFalse (by intro h; injection h; contradiction)
+
+instance: DecidableEq (Except String Bool) := Except.deq
+
+instance [BEq α] [BEq β] : BEq (Except α β) where
   beq := fun x y => match x, y with
     | Except.ok x, Except.ok y => x == y
     | Except.error x, Except.error y => x == y
     | _, _ => false
 
-def getOrExcept (message : String) (o : Option α) : Except String α :=
+def getOrThrow (message : String) (o : Option α) : Except String α :=
   match o with
   | some x => pure x
   | none => throw message
 
-#guard (getOrExcept "Error" (some 42) == Except.ok 42)
-#guard (getOrExcept "Error" (none : Option Int) == Except.error "Error")
+#guard (getOrThrow "Error" (some 42) == Except.ok 42)
+#guard (getOrThrow "Error" (none : Option Int) == Except.error "Error")