diff options
| -rw-r--r-- | Common/Nat.lean | 3 | ||||
| -rw-r--r-- | Common/Parsing.lean | 11 | ||||
| -rw-r--r-- | Day14.lean | 182 | ||||
| -rw-r--r-- | Main.lean | 2 | ||||
| -rw-r--r-- | inputs/day14.input | 100 | ||||
| -rw-r--r-- | lakefile.lean | 1 |
6 files changed, 299 insertions, 0 deletions
diff --git a/Common/Nat.lean b/Common/Nat.lean index 3a605a9..9d0ee29 100644 --- a/Common/Nat.lean +++ b/Common/Nat.lean @@ -20,3 +20,6 @@ theorem lt_of_pred_lt {a b : Nat} (h₁ : a < b.pred) : (a < b) := match b with | 0 => h₁ | _ + 1 => /-(Nat.pred_succ a).substr $-/ Nat.lt_succ_of_lt h₁ + +theorem lt_imp_pred_lt {a b : Nat} (h₁ : a < b) : (a.pred < b) := + Nat.lt_of_le_of_lt (Nat.pred_le a) h₁ diff --git a/Common/Parsing.lean b/Common/Parsing.lean index 3c5887a..c811319 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -47,6 +47,17 @@ def RectangularGrid.Get {grid : RectangularGrid Element} (coordinate : grid.Coor instance : GetElem (RectangularGrid Element) (RectangularGrid.Coordinate grid) Element (λg _ ↦ g = grid) where getElem := λ g c h ↦ g.Get (h▸c) +def RectangularGrid.set {grid : RectangularGrid Element} (coordinate : grid.Coordinate) (value : Element) : RectangularGrid Element := + let index := (Fin.cast grid.size_valid.symm coordinate.toIndex) + { + grid with + elements := grid.elements.set index value + size_valid := (grid.elements.size_set index value).substr grid.size_valid + } + +theorem RectangularGrid.set_same_size {grid : RectangularGrid Element} (coordinate : grid.Coordinate) (value : Element) : (grid.set coordinate value).width = grid.width ∧ (grid.set coordinate value).height = grid.height := + ⟨rfl,rfl⟩ + instance [ToString Element] : ToString (MaybeEmptyRectangularGrid Element) where toString := λe ↦ Id.run do let mut r := s!"Width: {e.width}, Height: {e.height}" diff --git a/Day14.lean b/Day14.lean new file mode 100644 index 0000000..bbaa616 --- /dev/null +++ b/Day14.lean @@ -0,0 +1,182 @@ +import «Common» + +namespace Day14 + +------------------------------------------------------------------------------------ + +inductive Tile +| Space +| Cube +| Round +deriving Repr, BEq + +instance : LawfulBEq Tile where + rfl := λ{a} ↦ by cases a <;> decide + eq_of_beq := by intros a b; cases a <;> cases b <;> simp <;> decide + +instance: ToString Tile where +toString := λ +| Tile.Space => "." +| Tile.Cube => "#" +| Tile.Round => "O" + +structure ParseCharError where +unexpectedCharacter : Char + +instance : ToString ParseCharError where +toString := λc ↦ s!"Unexpected Character '{c.unexpectedCharacter}', expected '.', '#', or 'O'." + +private def Tile.ofChar? : Char → Except ParseCharError Tile +| '.' => pure Tile.Space +| '#' => pure Tile.Cube +| 'O' => pure Tile.Round +| c => throw {unexpectedCharacter := c} + +abbrev ControlPanel := Parsing.RectangularGrid Tile + +abbrev ParseInputError := Parsing.RectangularGrid.ParseError ParseCharError + +def parse : String → Except ParseInputError ControlPanel := + Parsing.RectangularGrid.ofSubstring Tile.ofChar? ∘ String.toSubstring + +------------------------------------------------------------------------------------ + +/- +there's probably a better way, but I'm too lazy, so I'll just move them row-by-row. +pseudocode +for(row) + for(column) + if(tile == Round) + moveTileAsFarNorthAsPossible +-/ + +/-- Finds the northmost free space reachable from start. Does not look at start. -/ +private def findNorthmostFreeTile {controlPanel : ControlPanel} (start : controlPanel.Coordinate) : controlPanel.Coordinate := + if start.y > ⟨0,controlPanel.not_empty.right⟩ then + let northNeighbour := { start with y := ⟨start.y - 1,Nat.lt_imp_pred_lt start.y.isLt⟩ } + match controlPanel[northNeighbour] with + | Tile.Space => findNorthmostFreeTile northNeighbour + | Tile.Round | Tile.Cube => start + else + start +termination_by start.y + +private def moveTileNorth {controlPanel : ControlPanel} (position : controlPanel.Coordinate) : ControlPanel := + match controlPanel[position] with + | Tile.Space | Tile.Cube => controlPanel + | Tile.Round => + let intermediate := controlPanel.set position Tile.Space + let positionInIntermediate : intermediate.Coordinate := {x := position.x, y := position.y} -- how? well, I won't complain + let northMost := findNorthmostFreeTile positionInIntermediate + intermediate.set northMost Tile.Round + +private theorem moveTileNorth_same_size {controlPanel : ControlPanel} (position : controlPanel.Coordinate) : (moveTileNorth position).width = controlPanel.width ∧ (moveTileNorth position).height = controlPanel.height := by + constructor + all_goals + unfold moveTileNorth + match controlPanel[position] with + | Tile.Space | Tile.Cube => trivial + | Tile.Round => + simp only[Parsing.RectangularGrid.set_same_size] + +/- +-- Old solution, without do-notation. Proven to terminate, but needs a lot more code... + +/- had to move this to top level function to be able to prove stuff with it... "Declaration contains metavariables" -/ +private def moveAllTilesNorth_handleColumns (cp : ControlPanel) (row : Fin cp.height) (column : Fin cp.width) : ControlPanel := + let intermediate := moveTileNorth {x := column, y := row : cp.Coordinate} + let nextIndex := column.val + 1 + if h : nextIndex < intermediate.width then + have h₁ : intermediate.height = cp.height := (moveTileNorth_same_size {x := column, y := row : cp.Coordinate}).right + moveAllTilesNorth_handleColumns intermediate (h₁▸row) ⟨nextIndex,h⟩ + else + intermediate + termination_by cp.width - column + decreasing_by + have h₂ := (moveTileNorth_same_size { x := column, y := row }).left + rw[h₂] at h ⊢ + exact Nat.sub_lt_of_gt (Nat.le_of_lt h) (Nat.lt_succ.mpr $ Nat.le_refl _) + +private theorem moveAllTilesNorth_handleColumns_same_height (cp : ControlPanel) (row : Fin cp.height) (column : Fin cp.width) : (moveAllTilesNorth_handleColumns cp row column).height = cp.height := by + unfold moveAllTilesNorth_handleColumns + simp + have h₂ := (moveTileNorth_same_size { x := column, y := row }).right + split + case isFalse => exact h₂ + case isTrue => + have := moveAllTilesNorth_handleColumns_same_height (Day14.moveTileNorth { x := column, y := row }) (h₂ ▸ row) ⟨↑column + 1, by assumption⟩ + simp[h₂] at this + assumption + termination_by cp.width - column + decreasing_by + have h₂ := (moveTileNorth_same_size { x := column, y := row }).left + rename_i h + rw[h₂] at h ⊢ + exact Nat.sub_lt_of_gt (Nat.le_of_lt h) (Nat.lt_succ.mpr $ Nat.le_refl _) + +private def moveAllTilesNorth (controlPanel : ControlPanel) : ControlPanel := + handleRows (controlPanel) ⟨0,controlPanel.not_empty.right⟩ +where + handleRows (cp : ControlPanel) (row : Fin cp.height) : ControlPanel := + let intermediate := moveAllTilesNorth_handleColumns cp row ⟨0,cp.not_empty.left⟩ + let nextIndex := row.val + 1 + if h : nextIndex < intermediate.height then + handleRows intermediate ⟨nextIndex, h⟩ + else + intermediate + termination_by cp.height - row + decreasing_by + have h₁ : intermediate.height = cp.height := + moveAllTilesNorth_handleColumns_same_height cp row ⟨0,_⟩ + rw[h₁] at h ⊢ + exact Nat.sub_lt_of_gt (Nat.le_of_lt h) (Nat.lt_succ.mpr $ Nat.le_refl _) +-/ + +private def moveAllTilesNorth (controlPanel : ControlPanel) : ControlPanel := Id.run do + let mut result : ((c : ControlPanel) ×' (c.width = controlPanel.width ∧ c.height = controlPanel.height)) := ⟨controlPanel, ⟨rfl,rfl⟩⟩ + for hr :row in [:controlPanel.height] do + for hc : column in [:controlPanel.width] do + let x : Fin result.fst.width := Fin.cast result.snd.left.symm ⟨column,hc.upper⟩ + let y : Fin result.fst.height := Fin.cast result.snd.right.symm ⟨row,hr.upper⟩ + let coordinate : result.fst.Coordinate := {x, y} + have : (moveTileNorth coordinate).width = controlPanel.width ∧ (moveTileNorth coordinate).height = controlPanel.height := + (moveTileNorth_same_size coordinate).right.substr $ (moveTileNorth_same_size coordinate).left.substr result.snd + result := ⟨moveTileNorth coordinate, this⟩ + result.fst + +private def weightOnNorthSupport (controlPanel : ControlPanel) : Nat := Id.run do + let mut score := 0 + for hr :row in [:controlPanel.height] do + for hc : column in [:controlPanel.width] do + let coordinate := {x := ⟨column,hc.upper⟩, y := ⟨row,hr.upper⟩ : controlPanel.Coordinate} + if controlPanel[coordinate] == Tile.Round then + score := score + (controlPanel.height - row) + score + +def part1 : (input : ControlPanel) → Nat := weightOnNorthSupport ∘ moveAllTilesNorth + +------------------------------------------------------------------------------------ + +open DayPart +instance : Parse ⟨14, by simp⟩ (ι := ControlPanel) where + parse := Except.mapError toString ∘ parse + +instance : Part ⟨14,_⟩ Parts.One (ι := ControlPanel) (ρ := Nat) where + run := some ∘ part1 + +------------------------------------------------------------------------------------ + +private def testInput := "O....#.... +O.OO#....# +.....##... +OO.#O....O +.O.....O#. +O.#..O.#.# +..O..#O..O +.......O.. +#....###.. +#OO..#...." + +#eval parse testInput + +#eval (weightOnNorthSupport ∘ moveAllTilesNorth) <$> parse testInput @@ -12,6 +12,7 @@ import «Day10» import «Day11» import «Day12» import «Day13» +import «Day14» open DayPart @@ -50,6 +51,7 @@ def try_run_day_part (day : Days) (part : Parts) (data : String) : IO String := | ⟨12,_⟩, Parts.Two => try_run_day_part_impl ⟨12,_⟩ Parts.Two data | ⟨13,_⟩, Parts.One => try_run_day_part_impl ⟨13,_⟩ Parts.One data | ⟨13,_⟩, Parts.Two => try_run_day_part_impl ⟨13,_⟩ Parts.Two data + | ⟨14,_⟩, Parts.One => try_run_day_part_impl ⟨14,_⟩ Parts.One data | _, _ => throw $ IO.userError "The requested combination of day/part has not been implemented yet." def main (parameters : List String): IO Unit := do diff --git a/inputs/day14.input b/inputs/day14.input new file mode 100644 index 0000000..ac44ddf --- /dev/null +++ b/inputs/day14.input @@ -0,0 +1,100 @@ +...##OOOO...#..#.OO..#O........O.O.#..O........#...O#.O..#O.............O....#....O.O#.#.O......OO.O +O.......#..O.O.....O..O.OO.O#O..#.#.OO.OO.O.O.....O.#..O....O...O.......O..O#O.O.O.........O#OOO..OO +..O.OO..#...O#O.....O...##O.O..#...O##OO..#.O..#O#O...#.O.OO..#..#.#...........O..###...OOO##......O +O####O#....O.O##OO.O...#O...O.O...O#...O...#..#....#...OO.#.#.O#O..O..#O...#...#.....#.O#.O...##.... +#O..O..O..#.###.....O.#....O#...#..##..OO....OO.#.#O#O...O#..#........O.O....#...OO..O......#....... +O.O....O.#.......#.....O...........O..#.....#.O.....#...O.......O#.#.......O..#.........#......OO.O. +.O..#.......O.............#..O...##.OO##..O...#.....OO.O.#.....#.O..O..........#O#..##.#.#O#.O....#. +......O..O#O.##.O...#.##..OO....O#..#.O.##.OO...#..#.....O...#..OO.....OO.O......####..O.......O.#.O +...O.OO.....OO.#OO..#.....#......O.#....#.#...O....#.O#....O...O..#...##...O.#...#.O.....O#O...O.... +OO#.O..O...O.#......#.....O#.O..O.OO....#......#...O#...#.#..O..O...#.#.O#...OO#....OO#O.......#.... +O.....OO..#.#..#..O.#...........O.O..##.#.O.#.O.O.OO.O...O.O.O.OO##..O.......##.OO....O....OO....#OO +O..O#.O#.....####.#....#.##.OO..O...OO##....#.....#O.#O..#.O....#.O.#.O..O...##...O.......O.O..OO.#. +...O.#..O.O.....#..O##.....#OO.O............O......O.#..#.OO#....O.O..O........#.#.#O...O....#..OO#O +##.#.O##..#.##O....OOOO...#........#..O..OOO....O...O...O..O...O.O..OOO...##...O#O.O.OO.OOOOO#.#..## +...#..O.O##.O.#O.#..O#.#..O#..#...OO#...OOO.........O.O..O.#..O.....O.#........O....#...O....#..OO.# +.......#.#...#OO.O#..OO..OO.##.#O.OO.OO.OO.#....O..#O...#.O..O..O#.O.O.O.O...O#......O..O#....#...#. +....O....O#....OOO.....OO.#O......#.OO..O.#OO........O..O.O..O....OO...##..OO#.......#..OO.#O.O.##.O +OO.#...O.OO.#O#....##O#O.#....#.O.#.O.#.OO.....#...#.###.#.O..OO.O.O.OO.#.O#O...O.O#..OO...#O...OOO. +.......#....OO#..##O.#..O.O.O..#.#.#..OO.#..#.................O....OO##.##O..OO.O..#O.#.#..#.....O#O +..OO...O.O....O.O....O.O....#O.O....OO.........#..........#...#..OO...OO.......#.O...##.#.O.O##...OO +.OO.O#O.#....OOO..O.O.#..#O...O.O#.#O.O.##..##....#..OO.....#....#OO#.##........OOO.OO#O......#..O.# +...##.....#.........#.##..O.....#.O.#O.##..#..##O.OO#.....O#.......O.O..O#..O..#.....#....O......... +O....O....O.#...#...#OO#.O....#O##......O..#O..#..#..O#...O..O..#...OOOO#.OO..............O#....#.OO +.O.O..OO.##...OOO...O..OO.O....#.#....OO#O#......O#O.....O#.OO...OOOO..#....#..##..........#.O....O. +..#..O..#.......O#O..OO..O.........OOO..##....O..O..OO.#....O.....#.O.#.O.#.#OO#....#.....##.#O...O. +#....O.......O.#......OO.OO...O..O......#.O.O.O...#....#.#..#.O....#.#O.OOO..#.O..O.O.#.##........#. +OO..OO##..#.O..#OOO...O..O.O......O.#.#.O#....O#O#..O#........##.O#....OO..#O#..O..##.........O.#... +.OOO......O#.OO...........OO#..#.O.O..#...OO#...#.....#........O...O##....OO.....O..OOOO...#........ +O#.O....#.#..O.O..O.#.OOO.O..O......O.OOO..#..O..##..O.O....O.O.OO.##.....#.#O..##O..O......O##..#.. +#...#..O.OO..#.#.#......O.#..O.#.OO.#............#O#....#....O.......O...O....###....O.#.#O...OO#O.O +O..O..#....O.#.O..#.O.#.#OO#...O.O..#...O.#O......OO.O.O.....O...OO.#O#......#..#.......O#...#..O... +..O..O.#O.O#.##O..#OOO.O#.O.#....O.##.#..O..O...#......O..#O..OO....#O#..#O#.#OOO.#O.OO......OO#.... +#.....O#O..O..O.OO.#.......O........O.OO.#OO........O...O......O..O.O.......#.#....O#..O..#.....##.. +.....O.......#........OO...OOO#.#.#.#.O..##..O........#O.#.#O.#..#O.....#O....OO.......#......O....O +....#..#..O.#..#O#O..O....O..#.#....#..##.........O..O.#O.O..OO...O.##....#.O.#.#OOO..O..#.....#..O. +.#OO......O...#..##.O...#.O..........#.##.O....OO.O#....O.OOO....O..OO...#.#.O#...OO.O#O#O......#.## +O....O.#....O.#......OO.##..O..#...O.#..#..O....#..##...#....#........OO.......#..O.#.#...#..O...... +.#.#..O..O.#..#.O.#O..#..O....O...OO.#.#...OO.##..##.O..O..O..O.#...O.#OO##O..#.O.....#.##..O....O.. +..##................O#O#....#..#O.O....##.#...O...O.....#.....OO.#.#............OO#....O.#.O.O...O#. +.#..O.O...#O.O....#O....OO.#..O#...........O#.....##.O..#OO...#...O.OO.........OOOO.O...##.#....O##. +..O.......OOO...O.#OO.#......O.O......O.....O.OO......O#..#OO..#.O.......O.#.#.....#.O.O#O..O...O.#O +#............O#..O..O#.....#.O.#.O...O....#O..#...O........##OO..O.OO.OO.....O...###O.O#..#.##....#. +..#O..#.#...O......O......O....#.##O#.O.#OOO.....O..#.O.....#O..#..#.O.O...O..#.....#....#.......OO# +#..O..#O..#.O........###....OO.O.O...OOO#..OO.#..O...#..O...O#...O..O.O.O..O.......OO.O#..O..O...O.# +OO.OO.#OO.........O...#.OO.OO#..OO...#.....#O.O.O..#O..#.....O..##......O###O.......#.##..O......... +.#..O..O.O..OO.O..OOO..#...#.#..O.....O.....#.#...OO....O..#.OO#..##O#..OO.O...O..O...###.#..O#...O. +O...O.O................#....#...O#.#.#O#.O..#O..OO.O.OOO...O...O.OO.....#.OO..#.....#.....#.O.....OO +O...O..##O...####O###....O##O..O#.O.........#..O..O.###......O#..O...O#O...O#...O......O.O#..O.#...# +O..#.O...O.#..##O.#.....O........O.......OOO....#...#..O..#...##....#.##.O.O..#....O#...O.....#..OOO +O..#O#...O..O.O#....#...O..O..#....O.O..#.O..#O.......O#.O.........O.#.#..O.....O....#.OO.O........O +..#.........O..#OO.#O...O..#..O.#.O.O...O####........OO.##.O..#.#..#.#O#.OO..O.#.O..OOO...O..O...O.. +...#.....#.#...O.#.O#...O#..#.O....#.....#......O....#O#..O#O........O#....###OO....#...O##......#O# +..#.#..O.O#......O.O.OO........#O.#O..#.O#O......O.........O#O...#..#........#.....O............OOO. +.#O...####O#...#..O#..OO.O.OO..##O.#O...#...O....O.#......O..O...O..O.#..OO..#..#.##OO#.#..O......## +#..O.#.O..#.O#O#.O.#....O#..#.O.O...OO#O..O#.O.##O.O.OO......O##..###.O#....O..O.#.##.OO.O#OO....#.. +..O#.O....O.....#....OO#.O.....OO.#..OO..O....O..#..#O.#OO...O..O....##.O#.OOO.O#...#O..O..##O..OOO. +O...#........OO.OO.#O......#O..........##....O.#......O..#O.....O...#...O.O.#....##.....##.O.O.#..## +...O#..O.O.....OO.O......#.OO.O...O..O###OO....O.......#.O.OO..#O#...#.....#.........#OO......O..OOO +##...O..#OOO..O.#.O.O#..OOO##..O.....O#..O.OO........OO...O..#..O..###..#....O#.#.#......#.......... +..#.O.OOO..OO#..#....O.#.O..O.#.#.........OO...##......#.O.O#O...O...O.O.#..........##....#.#..O#..# +#...O#.....O..O........#...#.#.#O.##O#.O.#O..O.......O#...#.#.......##.#..OO...#.#O#..#.O..O.......# +.##.OO.#.#.#.O.#.........O..O.O#O...OO.....#..#OOO.#...O....O....O...##O.#O....OO.#O........###OO#.. +.##............O.#O.#O.....##..O.#...#.....O.OOO............O..#.#........#...#.O..#..#...#O..#..... +##O#..##O....#OO..#..#OOO..O.#OO.#..#..#OO#.OO.#.OO..O....OOO...O...O....O...O........#......#...O.. +#.#O.....#.OOO#O#...#.O....#O...#.OO.OO.O..O#.O##.O.O.O.O..O......#..OO...#O..O##.......O...O#O#O..# +#.....O...........O....#O##.O...O...........#..O...OO.###..OO.........OO..O.#....##.##.##...#.#...O. +O.#....OO#..O..OO.#O..OO...#O....O.O.OOOO##.#.....O..O........O.#....##O#..#..#.#..O.O....OO...O.... +..#O.#...#.O.#O.O..O.O#.......#.#...O.#......##OO..##O..O.O...#O...........O.#.#..O.O...O......O...# +.O....#O#.OO#..#.......#.O.....#......#OOO..O#..OO.....O.O...O..O#...OO.......#.O.#.O#........O.O..O +O....O.O.#.OO........O#..#..O.O...#......#...#...##.#.O#...OO.....#O#...#..#....O.O#.#.#....O..O.... +OO#.#..#OO###.O...#.O.#..#OOO.O....O..OO..O...O.#O#...#O.O.O.O..#O..O...##...O.#O...O....OO..O..#.OO +OOO....#OO....O..O#O.#O.....O#...O.#..O....O.....#O..........O#.#.#.OO.....O.....O.##.........O....# +.OO..#....#O..O.......O.##.O.......#.....#.....O.O..........#.O.O.O..#....#..#....O..#......#...O.O. +..#.#.#....OO.O#O..O#.#...OO..O.#OO..#O.##......#...#.O......#..#O.#O.#..O.#..O.........#.#........O +...O#.OO#.###.#..O.#...O..O#.O....#..O..O.#O.O........#..O..O..#.#.#OO.OO##O#............#..OOO#.O.. +....#..OO.O...O#.#.##O.O...O#...#.##.#.###...O..O...#...#...#..#.#O...#.........#.#.O.O#O..O..O#O... +.#.......O#O.#..##.OO#..OO..##...O#O.#.O...##..O..OO..#...O.#..#..........#....O...#....O.#.#...O... +..O..O..#.O..OO..O.##.O.OO.#.O.O....O.#O#.#.O..#.O...O.#...#O...#..O.......O....#O#..O..#OO...##.... +..O....O..OOO........OO..#..#..O.#...#.##OO...O...OOO..###O#.O.OO#.....O#...........OOO..OOOO.#O..## +.##.O##.#O.#..O......#.....O...#....O.O..#.......#...O..#.OOOO..#.#.##.#..O.....O...#.#..OO..#O#..O. +O.......O..O.O...O..#....O.#...OO........#....#O...O..OO....#...O.#O...OO....#.##O......#.O.O....OOO +O........O##..#.OO.O...#..OO..OO....#.O.O#.#..........OOO.#.O..###.#O..##...........O.#.O....#...O.O +..O.#OO...O..#...O###..O.#...O........#O.O...#.O#..#O..........O...#O...#...#.O..O....#O###.....#... +.OO#O###.O##O.O...O#...#..O#.........#..#.#.#OO#...O#O...#....##.#..#.O.OO...O...O.#O.OO.OO.#...O..O +OO.O.O#...O...#O#O.OOO...O....#OO..OO....O...#..O.O.O....#.O#.......O.#.O..#.O.#O..O..#O.O..O.O##O.# +.......#.....O.#....O.O.O.#..O#O#....O..O........O...OO...O.O.O.##.O..O.......#..........O#.#O..#... +.O..OO..O##......##......OOO........O...O..O.O##..#...O.O.#O#.#...#..........#.O...#O.OO...O....##.. +O........#...OO#....O..#OOO.O.#.#.O..O......O..O.O#.....#....O.....####.........#O...#O.####.OO..... +#..#O...#.#......OOO.OO..O#.O..O....#........O.......#.O........O..........O...O..#.....#O#.O.#..OO. +O#.....#OO......#..O..#.##OO.O..#.#O.OO....O..O.#....O.......###..#OO...#..O#.............O......... +O....#..O.O.#O#....O#...###.#O.#........O...#.......#.O.#O.#OO#OO.#O#....#O.....#.O##...O..#.#...... +.##......O....###...........O......#.....O..#.O...#.OO.##O...O.O#....#O.##...#O.O#..O..OO.O...#.O.O. +.##.#..#.##.O#.#.....##...#.O..#..##...O..O..#.#.O...#O..#...O#..O.#...O..#..#.O#.O#.O.##.O.#.#..#.O +.O..O....O...#O..OO..##O.O...##..#....#.....OO.O.O.####O..OO.......#...#....OO...O..#O.#.#......#O.. +O...#..O.....#..#......##O#O#.O#OO...O#..O.#.OO.O#.O#O..#.O#.#......OO...O.....O....OO.OOO.#....O#.. +#..##..........O...#....#.....#OO......O#####.....O.....O##O..O#O..O...O.O......OOO..OO......O.O..#. +...O#...OO#......OO.O....#..O..#........O.O......#O..#.....O............O.....O##.OO..O..#.O.#...... +..OO...O.#..O..O..........##O.OOO.....O..O.#...#.#..........#..#O...O.O.#..#.#.O.O...O..##..#.OO.... +O.............O.####O...O...#.O...##.O#.O.O..OOO..OO..#...#....#.O..O##...#..##...O..#..O..###.#.#.O +...O.O.....O.....O.....#.O.O..OO...O..O....OO##.....#.O.....#.#.#...O#.....#OO....O..........#..#.O. diff --git a/lakefile.lean b/lakefile.lean index 0790965..dc94b7a 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -16,6 +16,7 @@ lean_lib «Day10» where lean_lib «Day11» where lean_lib «Day12» where lean_lib «Day13» where +lean_lib «Day14» where lean_lib «Common» where |