eraseIdx

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

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 :=