index
:
aoc-2023
feature/day17
main
Advent of Code 2023 - I'm still learning Lean4, so please don't judge.
Andreas Grois
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
*
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
*
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
*
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
*
Heap: Unfinished proof RemoveLastWithIndex returns consistent data.
Andreas Grois
2024-07-20
1
-0
/
+34
*
Minor: Replace some simp by simp only in BinaryHeap
Andreas Grois
2024-07-20
1
-57
/
+61
*
Remove CompleteTree.indexOfLast, add CompleteTree.heapRemoveLastWithIndex
Andreas Grois
2024-07-20
1
-60
/
+77
*
Heap: Further nomenclature improvements.
Andreas Grois
2024-07-19
1
-28
/
+28
*
Make CompleteTree.heapRemoveLast private.
Andreas Grois
2024-07-19
1
-40
/
+38
*
Heap: Nomenclature clarified. Push and Pop now do what is expected.
Andreas Grois
2024-07-19
1
-111
/
+111
*
Heap: Exchange return values of the remove/replace functions.
Andreas Grois
2024-07-19
1
-56
/
+56
*
Factor out proofs of CompleteTree.popLast for readability
Andreas Grois
2024-07-19
1
-52
/
+44
*
Heap: Minor cleanup. Do a TODO.
Andreas Grois
2024-07-17
1
-92
/
+68
*
Finish BinaryHeap.RemoveAt.
Andreas Grois
2024-07-16
1
-25
/
+119
*
Continue on CompleteTree.heapReplaceElementAtIsHeap. Nearly done.
Andreas Grois
2024-07-15
1
-13
/
+72
*
Further work on heapReplaceElementAtIsHeap
Andreas Grois
2024-07-14
1
-2
/
+23
*
Continue at CompleteTree.heapReplaceElementAtIsHeap
Andreas Grois
2024-07-14
1
-1
/
+22
*
BinaryHeap.RemoveRoot added, and some proofs cleaned up a bit
Andreas Grois
2024-07-14
1
-22
/
+26
*
Finish CompleteTree.heapReplaceRootIsHeap.
Andreas Grois
2024-07-14
1
-9
/
+42
[next]