aoc-2023 - Advent of Code 2023 - I'm still learning Lean4, so please don't judge.

	Commit message (Collapse)	Author	Age	Files	Lines
*	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	1	-6/+0
\|
*	More cleanup of code in BinaryHeap.	Andreas Grois	2023-12-18	1	-55/+1
\| \| \| \| \|	Finally the propositions about even and odd numbers are no longer decidable. Not that I accidentally use them in runtime code!
*	Partial cleanup of Heap	Andreas Grois	2023-12-18	1	-119/+25
\|
*	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	-0/+172