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

	Commit message (Collapse)	Author	Age	Files	Lines
*	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
\| \| \| \| \|	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	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
\| \| \| \|	And fix an off-by-one in day 5
*	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