summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
...
* CompleteTree.replaceElementAt finished - now needs proofAndreas Grois2024-06-301-22/+40
|
* Partial implementation of CompleteTree.removeAtIndexAndreas Grois2024-06-302-3/+66
|
* CompleteTree.popLastIsHeap finished.Andreas Grois2024-06-291-2/+14
|
* Continue on popLast proof. popLastLeavesRoot finished.Andreas Grois2024-06-281-13/+59
|
* Continue on popLast validity proof. Still incomplete.Andreas Grois2024-06-271-5/+57
|
* Heap: Trivial part of popLastIsHeap proof.Andreas Grois2024-03-311-0/+16
|
* Make BinaryTree.PopLast function work with unfoldAndreas Grois2024-01-301-32/+34
| | | | at the cost of making it harder to read.
* Make Find function take a predicate. Simplify PopLast.Andreas Grois2024-01-251-27/+26
|
* Minor, rename wellDefinedLt to wellDefinedLeAndreas Grois2024-01-131-4/+4
|
* Change heap from less-than to less-than-or-equal.Andreas Grois2024-01-131-148/+83
| | | | | This not only simplifies the proofs, it also makes the structure easier to use.
* Fix Heap Insert preserves Heap Proof. Preconditions were wrong.Andreas Grois2024-01-131-18/+59
| | | | | | | | And with wrong I mean "unfulfillable if any elements in the heap should be equal to each other". I'm still not fully happy with this, as it relies on lt being compatible with Eq, but yeah, it works for now.
* Rename not_equal to antisymm, because that's what it is.Andreas Grois2024-01-101-7/+7
|
* (Finally) rename BalancedTree to CompleteTreeAndreas Grois2024-01-101-52/+52
|
* Implement actual BinaryHeap.insert function.Andreas Grois2024-01-101-0/+6
|
* Proof that heap insert preserves a heap is done!Andreas Grois2024-01-101-3/+73
|
* Heap.insert: Insert-Left is proven now.Andreas Grois2024-01-101-7/+45
|
* More progress on heap.insert proofAndreas Grois2024-01-091-8/+25
|
* Further progress on heap insert proof.Andreas Grois2024-01-081-12/+10
|
* Progress on the proof that heap.insert keeps the heap intact.Andreas Grois2024-01-081-0/+17
|
* Unfinished proof that insert keeps heap a heapAndreas Grois2024-01-051-31/+99
|
* Even more cleanup in HeapAndreas Grois2023-12-182-6/+6
|
* More cleanup of code in BinaryHeap.Andreas Grois2023-12-182-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 HeapAndreas Grois2023-12-183-119/+119
|
* Heap now has balancing conditions completeAndreas Grois2023-12-181-18/+174
|
* Heap: At least one subtree needs to be perfect now.Andreas Grois2023-12-151-13/+113
|
* Rename file to BinaryHeap, as it isn't a BTreeAndreas Grois2023-12-132-30/+30
|
* BinTreeHeap: Add condition le m nAndreas Grois2023-12-121-19/+51
|
* Incomplete Heap implementation.Andreas Grois2023-12-115-8/+146
|
* Day9: Simplify proof of terminationAndreas Grois2023-12-091-1/+1
|
* Day 9Andreas Grois2023-12-094-18/+284
|
* Fix Day 8 Part 2: Forgot to un-comment something.Andreas Grois2023-12-091-2/+2
| | | | While it doesn't change the result, it was technically wrong.
* Day 8 Part 2Andreas Grois2023-12-095-17/+156
|
* Not working Day8 Part 2.Andreas Grois2023-12-082-21/+52
| | | | Seems we need to be smarter.
* Day 8 Part 1Andreas Grois2023-12-084-2/+893
|
* Day 7Andreas Grois2023-12-088-0/+1243
|
* Day 6Andreas Grois2023-12-073-9/+82
|
* Allow error messages in parsing (for debugging)Andreas Grois2023-12-0710-33/+62
| | | | And fix an off-by-one in day 5
* Part 2, finallyAndreas Grois2023-12-062-17/+66
|
* Part of Day5 Part 2Andreas Grois2023-12-061-54/+105
|
* Day5, part 1Andreas Grois2023-12-065-5/+475
|
* Day 4Andreas Grois2023-12-044-0/+277
| | | | I'm particularly proud of part 2.
* Day 3: Fix swapped adjacents.Andreas Grois2023-12-031-11/+11
|
* Day 3, minor cleanupAndreas Grois2023-12-031-31/+12
|
* Day 3Andreas Grois2023-12-038-1/+319
|
* Quicksort. Might be useful later.Andreas Grois2023-12-032-0/+25
|
* Day 2Andreas Grois2023-12-027-3/+208
|
* Day 1Andreas Grois2023-12-0110-0/+1165
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 15:28:35 +0000