From ce7214e07a766bc1e5ab02346e42eb6ca441c509 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 22 Nov 2024 22:10:48 +0100
Subject: Fix deprecation warnings for Lean 4.13

---
 Day12.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Day12.lean')

diff --git a/Day12.lean b/Day12.lean
index f679f89..25fd28a 100644
--- a/Day12.lean
+++ b/Day12.lean
@@ -110,7 +110,7 @@ def mustFirstBeDamaged : (states : List SpringState) → Bool
 | .damaged :: _ => true
 | _ => false
 
-abbrev PossiblePositionsMemo := Lean.HashMap (List SpringState × List Nat) Nat
+abbrev PossiblePositionsMemo := Std.HashMap (List SpringState × List Nat) Nat
 
 def countPossiblePositionsWithDamagedMemoized (memo : PossiblePositionsMemo) (remainingSpace : List SpringState) (remainingDamagedGroups : List Nat) (h₁ : remainingDamagedGroups ≠ []) : (PossiblePositionsMemo × Nat) :=
   if h₂ : remainingSpace.isEmpty then
@@ -129,7 +129,7 @@ def countPossiblePositionsWithDamagedMemoized (memo : PossiblePositionsMemo) (re
             let d := (remainingSpace.drop g)
             if canFirstBeOperational d then
               let d := (d.drop 1)
-              if let some r := memo.find? (d, gs) then
+              if let some r := memo.get? (d, gs) then
                 (memo,r)
               else
                 let (memo, r) :=countPossiblePositionsWithDamagedMemoized memo d gs (List.ne_nil_of_not_empty.mp $ (Bool.not_eq_true _).mp h₃)
@@ -144,7 +144,7 @@ def countPossiblePositionsWithDamagedMemoized (memo : PossiblePositionsMemo) (re
           (memo, 0)
         else
           let remainingSpace := (remainingSpace.drop 1)
-          if let some r := memo.find? (remainingSpace, g :: gs) then
+          if let some r := memo.get? (remainingSpace, g :: gs) then
             (memo,r)
           else
             let (memo, r) := countPossiblePositionsWithDamagedMemoized memo remainingSpace (g :: gs) h₁
@@ -162,7 +162,7 @@ def countPossiblePositions (remainingSpace : List SpringState) (remainingDamaged
     else
       0
   else
-    Prod.snd $ countPossiblePositionsWithDamagedMemoized Lean.HashMap.empty remainingSpace remainingDamagedGroups (List.ne_nil_of_not_empty.mp $ (Bool.not_eq_true _).mp h)
+    Prod.snd $ countPossiblePositionsWithDamagedMemoized Std.HashMap.empty remainingSpace remainingDamagedGroups (List.ne_nil_of_not_empty.mp $ (Bool.not_eq_true _).mp h)
 
 
 def part1 (springs : List SpringArrangement) : Nat :=
-- 
cgit v1.2.3

