diff options
| -rw-r--r-- | Day10.lean | 10 | ||||
| -rw-r--r-- | Day14.lean | 6 | ||||
| -rw-r--r-- | Day3.lean | 2 | ||||
| -rw-r--r-- | Day8.lean | 2 | ||||
| -rw-r--r-- | lakefile.lean | 2 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
6 files changed, 12 insertions, 12 deletions
@@ -517,7 +517,7 @@ private theorem Area.ParseLine_start_at_tile (previous : Area.Raw) (pos : Nat) ( split at h₄; contradiction case isFalse h₇ => have h₈ : (previous.fields.push t)[previous.width * (previous.height - 1) + pos]! = t := by - have := Array.get_push_eq previous.fields t + have := Array.getElem_push_eq previous.fields t simp[h₂, Array.getElem!_eq_getElem] at this assumption have : t = Tile.start := beq_iff_eq.mp h₆ @@ -1018,8 +1018,8 @@ private def noSolution {area : Area} : (List $ Area.PathHead area) → Bool section ListMonad local instance : Monad List where - bind := List.bind - pure := List.pure + bind := List.flatMap + pure := List.singleton def part1 (area : Area) : List Nat := do let mut paths : List (Area.PathHead area) := area.pathStartsList @@ -1470,8 +1470,8 @@ private def PipeAtCoordinate.totalAndTransitiveLe (area : Area) : BinaryHeap.Tot section ListMonad -- We can do this here without perf issues. The list in question will never have more than 2 elements. local instance : Monad List where - pure := List.pure - bind := List.bind + pure := List.singleton + bind := List.flatMap private inductive WestEastFoldState (area : Area) | inside : Coordinate area.width area.height → WestEastFoldState area @@ -211,11 +211,11 @@ private def compareControlPanels (a b : ControlPanel) : Bool := /-- (Bad) Hash-Function for ControlPanel. It's good enough for this riddle, but that's about it. -/ private def hashControlPanel (p : ControlPanel) : UInt64 := Id.run do - let mut hash : UInt64 := mixHash ⟨Fin.ofNat' _ p.width⟩ ⟨Fin.ofNat' _ p.height⟩ + let mut hash : UInt64 := mixHash ⟨Fin.ofNat' UInt64.size p.width⟩ ⟨Fin.ofNat' UInt64.size p.height⟩ for hi : index in [:p.elements.size] do match p.elements[index] with - | Tile.Round => hash := mixHash hash ⟨Fin.ofNat' _ index⟩ - | Tile.Cube => hash := mixHash hash ⟨Fin.ofNat' _ (index + p.elements.size)⟩ + | Tile.Round => hash := mixHash hash ⟨Fin.ofNat' UInt64.size index⟩ + | Tile.Cube => hash := mixHash hash ⟨Fin.ofNat' UInt64.size (index + p.elements.size)⟩ | Tile.Space => continue hash @@ -103,7 +103,7 @@ def part2 (schematic : Schematic) : Nat := -- because here we need quick lookup for the numbers, not the parts. open Std(HashMap) in let numberCoordinates : HashMap Coordinate PartNumber := - HashMap.ofList $ schematic.numbers.bind $ λ pn ↦ pn.positions.map (·, pn) + HashMap.ofList $ schematic.numbers.flatMap $ λ pn ↦ pn.positions.map (·, pn) let gearSymbols := schematic.parts.filter (Part.symbol · == '*') -- but the symbols aren't enough, they need to be adjacent to **exactly** 2 numbers let numbersNextGearSymbols := List.eraseReps <$> gearSymbols.map λgs ↦ @@ -290,7 +290,7 @@ private def findFirstCommonCyclingGoal (waypoints : Std.HashMap WaypointId Conne let cyclingGoals := startPositions.map $ findCyclingGoalsInPath waypoints instructions possibleStarts let combinedGoals : List CyclingGoal := match cyclingGoals with | [] => [] - | g :: gs => flip gs.foldl g λc n ↦ c.bind λ cc ↦ n.filterMap λ nn ↦ nn.combine cc + | g :: gs => flip gs.foldl g λc n ↦ c.flatMap λ cc ↦ n.filterMap λ nn ↦ nn.combine cc let cyclingGoalStarts := combinedGoals.map CyclingGoal.start cyclingGoalStarts.min? diff --git a/lakefile.lean b/lakefile.lean index 1d653ed..78bd995 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -31,4 +31,4 @@ lean_exe «aoc-2023» where supportInterpreter := true require BinaryHeap from git - "https://github.com/soulsource/BinaryHeap"@"14c98def3901492d733d81a45a29c4009bc01435" + "https://github.com/soulsource/BinaryHeap"@"9a4169ce63e9d1c0e3e909174cbc43bd53526ae4" diff --git a/lean-toolchain b/lean-toolchain index b06a535..cb2924f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.13.0 +leanprover/lean4:4.14 |