From 3e9ab8b679faa68bf41addedae1ec0f963ee466a Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 1 Dec 2024 16:12:52 +0100 Subject: Day15, Part1 --- Day15.lean | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 Day15.lean (limited to 'Day15.lean') diff --git a/Day15.lean b/Day15.lean new file mode 100644 index 0000000..dcc5f3b --- /dev/null +++ b/Day15.lean @@ -0,0 +1,29 @@ +import Common + +namespace Day15 +------------------------------------------------------------------------------------ + +def parse (input : String) : List Substring := input.toSubstring.trim.splitOn "," + +------------------------------------------------------------------------------------ + +private def holidayAsciiStringHelper (currentValue : UInt8) (input : Substring) : UInt8 := + input.foldl (λ(v : UInt8) (c : Char) ↦ 17*(c.toUInt8 + v)) currentValue + +def part1 (input : List Substring) : Nat := + input.foldl (λc v ↦ c + (holidayAsciiStringHelper 0 v).toNat) 0 + +------------------------------------------------------------------------------------ + +open DayPart +instance : Parse ⟨15, by simp⟩ (ι := List Substring) where + parse := Except.ok ∘ parse + +instance : Part ⟨15,_⟩ Parts.One (ι := List Substring) (ρ := Nat) where + run := some ∘ part1 + +------------------------------------------------------------------------------------ + +private def testInput := "rn=1,cm-,qp=3,cm=2,qp-,pc=4,ot=9,ab=5,pc-,pc=6,ot=7" + +#eval parse testInput |> part1 -- cgit v1.2.3