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
path:
root
/
Common
Commit message (
Expand
)
Author
Age
Files
Lines
*
CompleteTree.popLastIsHeap finished.
Andreas Grois
2024-06-29
1
-2
/
+14
*
Continue on popLast proof. popLastLeavesRoot finished.
Andreas Grois
2024-06-28
1
-13
/
+59
*
Continue on popLast validity proof. Still incomplete.
Andreas Grois
2024-06-27
1
-5
/
+57
*
Heap: Trivial part of popLastIsHeap proof.
Andreas Grois
2024-03-31
1
-0
/
+16
*
Make BinaryTree.PopLast function work with unfold
Andreas Grois
2024-01-30
1
-32
/
+34
*
Make Find function take a predicate. Simplify PopLast.
Andreas Grois
2024-01-25
1
-27
/
+26
*
Minor, rename wellDefinedLt to wellDefinedLe
Andreas Grois
2024-01-13
1
-4
/
+4
*
Change heap from less-than to less-than-or-equal.
Andreas Grois
2024-01-13
1
-148
/
+83
*
Fix Heap Insert preserves Heap Proof. Preconditions were wrong.
Andreas Grois
2024-01-13
1
-18
/
+59
*
Rename not_equal to antisymm, because that's what it is.
Andreas Grois
2024-01-10
1
-7
/
+7
*
(Finally) rename BalancedTree to CompleteTree
Andreas Grois
2024-01-10
1
-52
/
+52
*
Implement actual BinaryHeap.insert function.
Andreas Grois
2024-01-10
1
-0
/
+6
*
Proof that heap insert preserves a heap is done!
Andreas Grois
2024-01-10
1
-3
/
+73
*
Heap.insert: Insert-Left is proven now.
Andreas Grois
2024-01-10
1
-7
/
+45
*
More progress on heap.insert proof
Andreas Grois
2024-01-09
1
-8
/
+25
*
Further progress on heap insert proof.
Andreas Grois
2024-01-08
1
-12
/
+10
*
Progress on the proof that heap.insert keeps the heap intact.
Andreas Grois
2024-01-08
1
-0
/
+17
*
Unfinished proof that insert keeps heap a heap
Andreas Grois
2024-01-05
1
-31
/
+99
*
Even more cleanup in Heap
Andreas Grois
2023-12-18
2
-6
/
+6
*
More cleanup of code in BinaryHeap.
Andreas Grois
2023-12-18
2
-55
/
+61
*
Partial cleanup of Heap
Andreas Grois
2023-12-18
2
-119
/
+118
*
Heap now has balancing conditions complete
Andreas Grois
2023-12-18
1
-18
/
+174
*
Heap: At least one subtree needs to be perfect now.
Andreas Grois
2023-12-15
1
-13
/
+113
*
Rename file to BinaryHeap, as it isn't a BTree
Andreas Grois
2023-12-13
1
-29
/
+29
*
BinTreeHeap: Add condition le m n
Andreas Grois
2023-12-12
1
-19
/
+51
*
Incomplete Heap implementation.
Andreas Grois
2023-12-11
1
-0
/
+140
*
Day 8 Part 2
Andreas Grois
2023-12-09
2
-13
/
+11
*
Day 7
Andreas Grois
2023-12-08
3
-0
/
+27
*
Day 6
Andreas Grois
2023-12-07
1
-0
/
+4
*
Allow error messages in parsing (for debugging)
Andreas Grois
2023-12-07
1
-1
/
+1
*
Day5, part 1
Andreas Grois
2023-12-06
1
-5
/
+7
*
Day 3
Andreas Grois
2023-12-03
2
-1
/
+29
*
Quicksort. Might be useful later.
Andreas Grois
2023-12-03
1
-0
/
+24
*
Day 2
Andreas Grois
2023-12-02
1
-0
/
+4
*
Day 1
Andreas Grois
2023-12-01
3
-0
/
+21