summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Day 14, Part 1.Andreas Grois2024-11-286-0/+299
|
* Day13 Part2Andreas Grois2024-11-262-16/+34
|
* Day 13, Part 1Andreas Grois2024-11-255-0/+1555
|
* Fix deprecation warnings for Lean 4.13Andreas Grois2024-11-225-27/+27
|
* Update to Lean 4.13Andreas Grois2024-11-223-13/+11
|
* Day 12 Part 2Andreas Grois2024-09-242-20/+44
|
* Day 12 Part 1.Andreas Grois2024-09-243-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 Day12Andreas Grois2024-09-236-7/+1103
|
* Begin Day12Andreas Grois2024-09-232-0/+37
|
* Day11: Comment out test codeAndreas Grois2024-09-191-16/+16
|
* Day11Andreas Grois2024-09-192-19/+74
|
* Continue a bit with Day 11 Part 1Andreas Grois2024-09-192-4/+75
|
* Day 11 ParsingAndreas Grois2024-09-195-24/+276
|
* Continue Day11/ParsingAndreas Grois2024-09-182-0/+37
|
* Begin Day 11.Andreas Grois2024-09-185-0/+52
|
* Revisit Day10 Part1 to account for multiple solutionsAndreas Grois2024-09-161-32/+50
|
* Day 10, Part 2Andreas Grois2024-09-164-100/+175
|
* Continue Day 10 Part 2. Solutions. Finally. But not final solutions.Andreas Grois2024-09-131-32/+138
|
* Continue Day10 Part2Andreas Grois2024-09-121-1/+88
|
* Continue Day10 Part 2Andreas Grois2024-09-111-24/+68
|
* Continue Day10 Part 2.Andreas Grois2024-09-111-48/+67
|
* Continue Day10 Part2Andreas Grois2024-09-111-12/+103
|
* Continue Day10 Part2Andreas Grois2024-09-101-36/+86
|
* Continue a bit on Day10 Part2Andreas Grois2024-09-101-17/+61
|
* Continue Day10 Part2Andreas Grois2024-09-093-6/+66
|
* Begin Day 10 Part 2Andreas Grois2024-09-081-11/+38
|
* Fix issue in Day10 Part1 end condition.Andreas Grois2024-09-081-1/+1
|
* Day 10 Part 1Andreas Grois2024-09-082-52/+76
|
* Begin implementing Day10 Part1Andreas Grois2024-09-082-34/+351
|
* Day 10 Parsing. If I don' want to prove the inverse, it's done.Andreas Grois2024-09-071-6/+100
|
* Parser for Day10, maybe done.Andreas Grois2024-09-053-14/+138
|
* Continue day10 input parsing proofsAndreas Grois2024-09-051-4/+80
|
* Contineu Area.ParseRaw_start_positionAndreas Grois2024-09-041-3/+19
|
* Unfinished rewrite of Area.parseAndreas Grois2024-09-041-45/+299
|
* First draft of input-parsing function for Day 10.Andreas Grois2024-09-022-1/+251
| | | | Fail to prove anything for it...
* Move BinaryHeap to its own Github project.Andreas Grois2024-09-015-1426/+4
|
* Heap: Nomenclature and namespace changes.Andreas Grois2024-07-211-25/+25
|
* Simplify CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndexAndreas Grois2024-07-211-78/+32
|
* Finish CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndexAndreas Grois2024-07-211-1/+105
|
* Heap: Unfinished proof RemoveLastWithIndex returns consistent data.Andreas Grois2024-07-201-0/+34
|
* Minor: Replace some simp by simp only in BinaryHeapAndreas Grois2024-07-201-57/+61
|
* Remove CompleteTree.indexOfLast, add CompleteTree.heapRemoveLastWithIndexAndreas Grois2024-07-201-60/+77
| | | | | indexOfLast was going through the tree the same way as heapRemoveLast did, so heapRemoveLast now can optionally compute the index.
* Heap: Further nomenclature improvements.Andreas Grois2024-07-191-28/+28
|
* Make CompleteTree.heapRemoveLast private.Andreas Grois2024-07-191-40/+38
| | | | | | | It's confusing, because it uses breadth-first indexing, and regular indices are depth-first. Also, it's not needed in the public API, as there is the removeAt function that can do the same.
* Heap: Nomenclature clarified. Push and Pop now do what is expected.Andreas Grois2024-07-191-111/+111
|
* Heap: Exchange return values of the remove/replace functions.Andreas Grois2024-07-191-56/+56
| | | | This makes it easier to extend them, due to the right-associativity of tuples.
* Factor out proofs of CompleteTree.popLast for readabilityAndreas Grois2024-07-191-52/+44
|
* Heap: Minor cleanup. Do a TODO.Andreas Grois2024-07-171-92/+68
|
* Finish BinaryHeap.RemoveAt.Andreas Grois2024-07-161-25/+119
| | | | There is still a helper in this that is very inefficient though...
* Continue on CompleteTree.heapReplaceElementAtIsHeap. Nearly done.Andreas Grois2024-07-151-13/+72
|
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 14:55:39 +0000