From b9f09d537b8a877b36638ed6dbd630bb8100a2b0 Mon Sep 17 00:00:00 2001
From: Matt Russell <MattRussellUK@gmail.com>
Date: Mon, 2 Dec 2024 08:45:44 +0000
Subject: [PATCH] eraseIdx

---
 Aoc2024/Day02/Solve.lean | 4 ++--
 Aoc2024/Utils.lean       | 8 --------
 2 files changed, 2 insertions(+), 10 deletions(-)

diff --git a/Aoc2024/Day02/Solve.lean b/Aoc2024/Day02/Solve.lean
index 0f79b3f..c8d598b 100644
--- a/Aoc2024/Day02/Solve.lean
+++ b/Aoc2024/Day02/Solve.lean
@@ -9,7 +9,7 @@ private def decreasingSlowly: HashSet Int := [-1, -2, -3].toSet
 
 private def isSafe (report : Report) : Bool :=
   let diffs := report.differences.toSet
-  diffs.isSubsetOf increasingSlowly || diffs.isSubsetOf decreasingSlowly
+  diffs.isSubsetOf increasingSlowly ∨ diffs.isSubsetOf decreasingSlowly
 
 #guard isSafe [7, 6, 4, 2, 1] == true
 #guard isSafe [1, 2, 7, 8, 9] == false
@@ -25,7 +25,7 @@ def parseAndSolvePart1 (s : String): Except String Int := parseReports s |>.map
 #guard parseAndSolvePart1 exampleInput == Except.ok 2
 
 private def isSafeWithTolerance (report : Report) : Bool :=
-  List.range report.length |>.map report.removeNth |>.any isSafe
+  List.range report.length |>.map report.eraseIdx |>.any isSafe
 
 #guard isSafeWithTolerance [7, 6, 4, 2, 1] == true
 #guard isSafeWithTolerance [1, 2, 7, 8, 9] == false
diff --git a/Aoc2024/Utils.lean b/Aoc2024/Utils.lean
index b86c332..e302306 100644
--- a/Aoc2024/Utils.lean
+++ b/Aoc2024/Utils.lean
@@ -52,9 +52,6 @@ namespace List
   def toSet {α:Type} [BEq α] [Hashable α] (xs: List α) : HashSet α :=
     HashSet.ofList xs
 
-  def removeNth (n: Nat) (xs: List α) : List α :=
-    xs.take n ++ xs.drop (n + 1)
-
   def differences (xs: List Int) : List Int :=
     xs.zip xs.tail |>.map (λ (a, b) => b - a)
 
@@ -66,11 +63,6 @@ end List
 #guard [1].differences == []
 #guard [1, 2, 3, 2, 5].differences == [1, 1, -1, 3]
 
-#guard [1, 2, 3].removeNth 0 == [2, 3]
-#guard [1, 2, 3].removeNth 1 == [1, 3]
-#guard [1, 2, 3].removeNth 2 == [1, 2]
-#guard [1, 2, 3].removeNth 3 == [1, 2, 3]
-
 namespace Std.HashSet
 
   def isSubsetOf [Hashable α] [BEq α] (xs: HashSet α) (ys: HashSet α) : Bool :=