| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Lean 4.14 | Andreas Grois | 2024-12-17 | 6 | -12/+12 |
| | | |||||
| * | Day 16 Part 2 | Andreas Grois | 2024-12-16 | 3 | -0/+76 |
| | | |||||
| * | Day 16, part 1 | Andreas Grois | 2024-12-15 | 2 | -7/+190 |
| | | |||||
| * | Begin Day16 | Andreas Grois | 2024-12-14 | 7 | -0/+332 |
| | | |||||
| * | Minor, indentation | Andreas Grois | 2024-12-01 | 1 | -1/+1 |
| | | |||||
| * | Change Day15 Part 2 to not use do-notation. | Andreas Grois | 2024-12-01 | 1 | -8/+10 |
| | | |||||
| * | Day 15, Part 2 | Andreas Grois | 2024-12-01 | 2 | -8/+129 |
| | | |||||
| * | Day15, Part1 | Andreas Grois | 2024-12-01 | 4 | -0/+33 |
| | | |||||
| * | Change all imports from Lean to Std to reduce binary size. | Andreas Grois | 2024-11-29 | 4 | -7/+7 |
| | | | | | | Reduces binary size by more than a factor of 10... https://github.com/leanprover/lean4/issues/5274 | ||||
| * | Minor optimization of day 14 part 2. | Andreas Grois | 2024-11-29 | 1 | -5/+9 |
| | | | | | | The previous code kept using the Part2Memory even after a cycle had been found. While this didn't break anything, it's a waste of CPU time. | ||||
| * | Day14 Part 2 | Andreas Grois | 2024-11-29 | 2 | -70/+180 |
| | | |||||
| * | Day 14, Part 1. | Andreas Grois | 2024-11-28 | 6 | -0/+299 |
| | | |||||
| * | Day13 Part2 | Andreas Grois | 2024-11-26 | 2 | -16/+34 |
| | | |||||
| * | Day 13, Part 1 | Andreas Grois | 2024-11-25 | 5 | -0/+1555 |
| | | |||||
| * | Fix deprecation warnings for Lean 4.13 | Andreas Grois | 2024-11-22 | 5 | -27/+27 |
| | | |||||
| * | Update to Lean 4.13 | Andreas Grois | 2024-11-22 | 3 | -13/+11 |
| | | |||||
| * | Day 12 Part 2 | Andreas Grois | 2024-09-24 | 2 | -20/+44 |
| | | |||||
| * | Day 12 Part 1. | Andreas Grois | 2024-09-24 | 3 | -10/+142 |
| | | | | | | God, I fell into the premature optimization trap here... But I'm glad I did, that should make part 2 way easier. | ||||
| * | Continue Day12 | Andreas Grois | 2024-09-23 | 6 | -7/+1103 |
| | | |||||
| * | Begin Day12 | Andreas Grois | 2024-09-23 | 2 | -0/+37 |
| | | |||||
| * | Day11: Comment out test code | Andreas Grois | 2024-09-19 | 1 | -16/+16 |
| | | |||||
| * | Day11 | Andreas Grois | 2024-09-19 | 2 | -19/+74 |
| | | |||||
| * | Continue a bit with Day 11 Part 1 | Andreas Grois | 2024-09-19 | 2 | -4/+75 |
| | | |||||
| * | Day 11 Parsing | Andreas Grois | 2024-09-19 | 5 | -24/+276 |
| | | |||||
| * | Continue Day11/Parsing | Andreas Grois | 2024-09-18 | 2 | -0/+37 |
| | | |||||
| * | Begin Day 11. | Andreas Grois | 2024-09-18 | 5 | -0/+52 |
| | | |||||
| * | Revisit Day10 Part1 to account for multiple solutions | Andreas Grois | 2024-09-16 | 1 | -32/+50 |
| | | |||||
| * | Day 10, Part 2 | Andreas Grois | 2024-09-16 | 4 | -100/+175 |
| | | |||||
| * | Continue Day 10 Part 2. Solutions. Finally. But not final solutions. | Andreas Grois | 2024-09-13 | 1 | -32/+138 |
| | | |||||
| * | Continue Day10 Part2 | Andreas Grois | 2024-09-12 | 1 | -1/+88 |
| | | |||||
| * | Continue Day10 Part 2 | Andreas Grois | 2024-09-11 | 1 | -24/+68 |
| | | |||||
| * | Continue Day10 Part 2. | Andreas Grois | 2024-09-11 | 1 | -48/+67 |
| | | |||||
| * | Continue Day10 Part2 | Andreas Grois | 2024-09-11 | 1 | -12/+103 |
| | | |||||
| * | Continue Day10 Part2 | Andreas Grois | 2024-09-10 | 1 | -36/+86 |
| | | |||||
| * | Continue a bit on Day10 Part2 | Andreas Grois | 2024-09-10 | 1 | -17/+61 |
| | | |||||
| * | Continue Day10 Part2 | Andreas Grois | 2024-09-09 | 3 | -6/+66 |
| | | |||||
| * | Begin Day 10 Part 2 | Andreas Grois | 2024-09-08 | 1 | -11/+38 |
| | | |||||
| * | Fix issue in Day10 Part1 end condition. | Andreas Grois | 2024-09-08 | 1 | -1/+1 |
| | | |||||
| * | Day 10 Part 1 | Andreas Grois | 2024-09-08 | 2 | -52/+76 |
| | | |||||
| * | Begin implementing Day10 Part1 | Andreas Grois | 2024-09-08 | 2 | -34/+351 |
| | | |||||
| * | Day 10 Parsing. If I don' want to prove the inverse, it's done. | Andreas Grois | 2024-09-07 | 1 | -6/+100 |
| | | |||||
| * | Parser for Day10, maybe done. | Andreas Grois | 2024-09-05 | 3 | -14/+138 |
| | | |||||
| * | Continue day10 input parsing proofs | Andreas Grois | 2024-09-05 | 1 | -4/+80 |
| | | |||||
| * | Contineu Area.ParseRaw_start_position | Andreas Grois | 2024-09-04 | 1 | -3/+19 |
| | | |||||
| * | Unfinished rewrite of Area.parse | Andreas Grois | 2024-09-04 | 1 | -45/+299 |
| | | |||||
| * | First draft of input-parsing function for Day 10. | Andreas Grois | 2024-09-02 | 2 | -1/+251 |
| | | | | | Fail to prove anything for it... | ||||
| * | Move BinaryHeap to its own Github project. | Andreas Grois | 2024-09-01 | 5 | -1426/+4 |
| | | |||||
| * | Heap: Nomenclature and namespace changes. | Andreas Grois | 2024-07-21 | 1 | -25/+25 |
| | | |||||
| * | Simplify CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndex | Andreas Grois | 2024-07-21 | 1 | -78/+32 |
| | | |||||
| * | Finish CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndex | Andreas Grois | 2024-07-21 | 1 | -1/+105 |
| | | |||||
